flatten-module
rule-to-lemma "++ []"

-- module main:Main where
--   absR :: forall a . ([a] -> H a) -> [a] -> [a]
--   repR :: forall a . ([a] -> [a]) -> [a] -> H a
--   rev :: forall a . [a] -> [a]
--   main :: IO ()
--   main :: IO ()

prove-lemma "++ []"

-- Goal:
-- forall * xs. (++) * xs ([] *) = xs

lhs (one-td (unfold-rule appendFix))

-- Goal:
-- forall *. (++) * = myAppend *

assume -- proven appendFix

-- Goal:
-- forall * xs. myAppend * xs ([] *) = xs

induction 'xs

-- Goal:
-- forall *. myAppend * (undefined *) ([] *) = undefined *

lhs unfold

-- Goal:
-- forall *.
-- case undefined * of wild *
--   [] -> [] *
--   (:) x xs -> (:) * x (myAppend * xs ([] *))
-- =
-- undefined *

lhs undefined-expr

-- Goal:
-- forall *. undefined * = undefined *

end-case -- proven "++ []-induction-case-undefined"

-- Goal:
-- forall *. myAppend * ([] *) ([] *) = [] *

lhs unfold

-- Goal:
-- forall *.
-- case [] * of wild *
--   [] -> [] *
--   (:) x xs -> (:) * x (myAppend * xs ([] *))
-- =
-- [] *

lhs simplify

-- Goal:
-- forall *. [] * = [] *

end-case -- proven "++ []-induction-case-[]"

-- Assumed lemmas:
-- ind-hyp-0 (Assumed)
--   myAppend * b ([] *) = b
-- Goal:
-- forall * a b. myAppend * ((:) * a b) ([] *) = (:) * a b

lhs unfold

-- Assumed lemmas:
-- ind-hyp-0 (Assumed)
--   myAppend * b ([] *) = b
-- Goal:
-- forall * a b.
-- case (:) * a b of wild *
--   [] -> [] *
--   (:) x xs -> (:) * x (myAppend * xs ([] *))
-- =
-- (:) * a b

lhs simplify

-- Assumed lemmas:
-- ind-hyp-0 (Assumed)
--   myAppend * b ([] *) = b
-- Goal:
-- forall * a b. (:) * a (myAppend * b ([] *)) = (:) * a b

lhs (one-td (lemma-forward ind-hyp-0))

-- Assumed lemmas:
-- ind-hyp-0 (Assumed)
--   myAppend * b ([] *) = b
-- Goal:
-- forall * a b. (:) * a b = (:) * a b

end-case -- proven "++ []-induction-case-:"
-- proven "++ []"
rule-to-lemma "repH []"

-- module main:Main where
--   absR :: forall a . ([a] -> H a) -> [a] -> [a]
--   repR :: forall a . ([a] -> [a]) -> [a] -> H a
--   rev :: forall a . [a] -> [a]
--   main :: IO ()
--   main :: IO ()

prove-lemma "repH []"

-- Goal:
-- forall *. repH * ([] *) = id *

lhs unfold

-- Goal:
-- forall *. (++) * ([] *) = id *

extensionality

-- Goal:
-- forall * x. (++) * ([] *) x = id * x

lhs (one-td (unfold-rule appendFix))

-- Goal:
-- forall * x. myAppend * ([] *) x = id * x

lhs unfold

-- Goal:
-- forall * x.
-- case [] * of wild *
--   [] -> x
--   (:) x xs -> (:) * x (myAppend * xs x)
-- =
-- id * x

both smash

-- Goal:
-- forall * x. x = x

end-proof -- proven "repH []"
rule-to-lemma "repH (:)"

-- module main:Main where
--   absR :: forall a . ([a] -> H a) -> [a] -> [a]
--   repR :: forall a . ([a] -> [a]) -> [a] -> H a
--   rev :: forall a . [a] -> [a]
--   main :: IO ()
--   main :: IO ()

prove-lemma "repH (:)"

-- Goal:
-- forall * x xs. repH * ((:) * x xs) = (.) * * * ((:) * x) (repH * xs)

both (any-call (unfold 'repH))

-- Goal:
-- forall * x xs. (++) * ((:) * x xs) = (.) * * * ((:) * x) ((++) * xs)

both (any-call (unfold-rule appendFix))

-- Goal:
-- forall * x xs. myAppend * ((:) * x xs) = (.) * * * ((:) * x) (myAppend * xs)

rhs unfold

-- Goal:
-- forall * x xs. myAppend * ((:) * x xs) = \ x -> (:) * x (myAppend * xs x)

lhs (unfold >>> smash)

-- Goal:
-- forall * x xs. \ ys -> (:) * x (myAppend * xs ys) = \ x -> (:) * x (myAppend * xs x)

end-proof -- proven "repH (:)"
rule-to-lemma "repH ++"

-- module main:Main where
--   absR :: forall a . ([a] -> H a) -> [a] -> [a]
--   repR :: forall a . ([a] -> [a]) -> [a] -> H a
--   rev :: forall a . [a] -> [a]
--   main :: IO ()
--   main :: IO ()

prove-lemma "repH ++"

-- Goal:
-- forall * xs ys. repH * ((++) * xs ys) = (.) * * * (repH * xs) (repH * ys)

both (any-call (unfold 'repH))

-- Goal:
-- forall * xs ys. (++) * ((++) * xs ys) = (.) * * * ((++) * xs) ((++) * ys)

both (any-call (unfold-rule appendFix))

-- Goal:
-- forall * xs ys. myAppend * (myAppend * xs ys) = (.) * * * (myAppend * xs) (myAppend * ys)

lhs (eta-expand 'x)

-- Goal:
-- forall * xs ys. \ x -> myAppend * (myAppend * xs ys) x = (.) * * * (myAppend * xs) (myAppend * ys)

rhs unfold

-- Goal:
-- forall * xs ys. \ x -> myAppend * (myAppend * xs ys) x = \ x -> myAppend * xs (myAppend * ys x)

induction 'xs

-- Goal:
-- forall * ys x. myAppend * (myAppend * (undefined *) ys) x = myAppend * (undefined *) (myAppend * ys x)

both (replicate 2 (any-call (unfold 'myAppend)))

-- Goal:
-- forall * ys x.
-- case case undefined * of wild *
--        [] -> ys
--        (:) x xs -> (:) * x (myAppend * xs ys)
--  of wild *
--   [] -> x
--   (:) x xs ->
--     (:) * x
--         (case xs of wild *
--            [] -> x
--            (:) x xs -> (:) * x (myAppend * xs x))
-- =
-- case undefined * of wild *
--   [] ->
--     case ys of wild *
--       [] -> x
--       (:) x xs ->
--         (:) * x
--             (case xs of wild *
--                [] -> x
--                (:) x xs -> (:) * x (myAppend * xs x))
--   (:) x xs ->
--     (:) * x
--         (case xs of wild *
--            [] ->
--              case ys of wild *
--                [] -> x
--                (:) x xs ->
--                  (:) * x
--                      (case xs of wild *
--                         [] -> x
--                         (:) x xs -> (:) * x (myAppend * xs x))
--            (:) x xs ->
--              (:) * x
--                  (myAppend * xs
--                            (case ys of wild *
--                               [] -> x
--                               (:) x xs ->
--                                 (:) * x
--                                     (case xs of wild *
--                                        [] -> x
--                                        (:) x xs -> (:) * x (myAppend * xs x)))))

both (innermost undefined-expr)

-- Goal:
-- forall * ys x. undefined * = undefined *

end-case -- proven "repH ++-induction-case-undefined"

-- Goal:
-- forall * ys x. myAppend * (myAppend * ([] *) ys) x = myAppend * ([] *) (myAppend * ys x)

both (replicate 2 (any-call (unfold 'myAppend)))

-- Goal:
-- forall * ys x.
-- case case [] * of wild *
--        [] -> ys
--        (:) x xs -> (:) * x (myAppend * xs ys)
--  of wild *
--   [] -> x
--   (:) x xs ->
--     (:) * x
--         (case xs of wild *
--            [] -> x
--            (:) x xs -> (:) * x (myAppend * xs x))
-- =
-- case [] * of wild *
--   [] ->
--     case ys of wild *
--       [] -> x
--       (:) x xs ->
--         (:) * x
--             (case xs of wild *
--                [] -> x
--                (:) x xs -> (:) * x (myAppend * xs x))
--   (:) x xs ->
--     (:) * x
--         (case xs of wild *
--            [] ->
--              case ys of wild *
--                [] -> x
--                (:) x xs ->
--                  (:) * x
--                      (case xs of wild *
--                         [] -> x
--                         (:) x xs -> (:) * x (myAppend * xs x))
--            (:) x xs ->
--              (:) * x
--                  (myAppend * xs
--                            (case ys of wild *
--                               [] -> x
--                               (:) x xs ->
--                                 (:) * x
--                                     (case xs of wild *
--                                        [] -> x
--                                        (:) x xs -> (:) * x (myAppend * xs x)))))

both smash

-- Goal:
-- forall * ys x.
-- case ys of wild *
--   [] -> x
--   (:) x xs ->
--     (:) * x
--         (case xs of wild *
--            [] -> x
--            (:) x xs -> (:) * x (myAppend * xs x))
-- =
-- case ys of wild *
--   [] -> x
--   (:) x xs ->
--     (:) * x
--         (case xs of wild *
--            [] -> x
--            (:) x xs -> (:) * x (myAppend * xs x))

end-case -- proven "repH ++-induction-case-[]"

-- Assumed lemmas:
-- ind-hyp-0 (Assumed)
--   \ x -> myAppend * (myAppend * b ys) x = \ x -> myAppend * b (myAppend * ys x)
-- Goal:
-- forall * ys a b x. myAppend * (myAppend * ((:) * a b) ys) x = myAppend * ((:) * a b) (myAppend * ys x)

both (one-td unfold)

-- Assumed lemmas:
-- ind-hyp-0 (Assumed)
--   \ x -> myAppend * (myAppend * b ys) x = \ x -> myAppend * b (myAppend * ys x)
-- Goal:
-- forall * ys a b x.
-- case myAppend * ((:) * a b) ys of wild *
--   [] -> x
--   (:) x xs -> (:) * x (myAppend * xs x)
-- =
-- case (:) * a b of wild *
--   [] -> myAppend * ys x
--   (:) x xs -> (:) * x (myAppend * xs (myAppend * ys x))

lhs (one-td unfold)

-- Assumed lemmas:
-- ind-hyp-0 (Assumed)
--   \ x -> myAppend * (myAppend * b ys) x = \ x -> myAppend * b (myAppend * ys x)
-- Goal:
-- forall * ys a b x.
-- case case (:) * a b of wild *
--        [] -> ys
--        (:) x xs -> (:) * x (myAppend * xs ys)
--  of wild *
--   [] -> x
--   (:) x xs -> (:) * x (myAppend * xs x)
-- =
-- case (:) * a b of wild *
--   [] -> myAppend * ys x
--   (:) x xs -> (:) * x (myAppend * xs (myAppend * ys x))

both smash

-- Assumed lemmas:
-- ind-hyp-0 (Assumed)
--   \ x -> myAppend * (myAppend * b ys) x = \ x -> myAppend * b (myAppend * ys x)
-- Goal:
-- forall * ys a b x. (:) * a (myAppend * (myAppend * b ys) x) = (:) * a (myAppend * b (myAppend * ys x))

rhs (one-td (lemma-backward ind-hyp-0))

-- Assumed lemmas:
-- ind-hyp-0 (Assumed)
--   \ x -> myAppend * (myAppend * b ys) x = \ x -> myAppend * b (myAppend * ys x)
-- Goal:
-- forall * ys a b x. (:) * a (myAppend * (myAppend * b ys) x) = (:) * a (myAppend * (myAppend * b ys) x)

end-case -- proven "repH ++-induction-case-:"
-- proven "repH ++"

-- module main:Main where
--   absR :: forall a . ([a] -> H a) -> [a] -> [a]
--   repR :: forall a . ([a] -> [a]) -> [a] -> H a
--   rev :: forall a . [a] -> [a]
--   main :: IO ()
--   main :: IO ()

binding-of 'rev

-- rev = \ * ds ->
--   case ds of wild *
--     [] -> [] *
--     (:) x xs -> (++) * (rev * xs) ((:) * x ([] *))

fix-intro

-- rev = \ * ->
--   fix *
--       (\ rev ds ->
--          case ds of wild *
--            [] -> [] *
--            (:) x xs -> (++) * (rev xs) ((:) * x ([] *)))

application-of 'fix

-- fix *
--     (\ rev ds ->
--        case ds of wild *
--          [] -> [] *
--          (:) x xs -> (++) * (rev xs) ((:) * x ([] *)))

split-1-beta rev [| absR |] [| repR |]

-- Goal:
-- fix *
--     ((.) * * * (absR *)
--          ((.) * * * (repR *)
--               (\ rev ds ->
--                  case ds of wild *
--                    [] -> [] *
--                    (:) x xs -> (++) * (rev xs) ((:) * x ([] *)))))
-- =
-- fix *
--     (\ rev ds ->
--        case ds of wild *
--          [] -> [] *
--          (:) x xs -> (++) * (rev xs) ((:) * x ([] *)))

both (unfold >>> smash)

-- Goal:
-- let rec x =
--           absR *
--                (repR *
--                      (\ ds ->
--                         case ds of wild *
--                           [] -> [] *
--                           (:) x xs -> (++) * (x xs) ((:) * x ([] *))))
-- in x
-- =
-- let rec x = \ ds ->
--           case ds of wild *
--             [] -> [] *
--             (:) x xs -> (++) * (x xs) ((:) * x ([] *))
-- in x

lhs (replicate 5 ((one-td unfold) >+> smash))

-- Goal:
-- let rec x = \ x ->
--           (++) *
--                (case x of wild *
--                   [] -> [] *
--                   (:) x xs -> (++) * (x xs) ((:) * x ([] *)))
--                ([] *)
-- in x
-- =
-- let rec x = \ ds ->
--           case ds of wild *
--             [] -> [] *
--             (:) x xs -> (++) * (x xs) ((:) * x ([] *))
-- in x

lhs (one-td (lemma-forward "++ []"))

-- Goal:
-- let rec x = \ x ->
--           case x of wild *
--             [] -> [] *
--             (:) x xs -> (++) * (x xs) ((:) * x ([] *))
-- in x
-- =
-- let rec x = \ ds ->
--           case ds of wild *
--             [] -> [] *
--             (:) x xs -> (++) * (x xs) ((:) * x ([] *))
-- in x

end-proof -- proven rev-assumption

-- let g =
--       (.) * * * (repR *)
--           ((.) * * *
--                (\ rev ds ->
--                   case ds of wild *
--                     [] -> [] *
--                     (:) x xs -> (++) * (rev xs) ((:) * x ([] *)))
--                (absR *))
--     worker = fix * g
-- in absR * worker

any-call (unfold ['absR,'repR])

-- let g =
--       (.) * * * (\ eta -> (\ f -> (.) * * * (repH *) f) eta)
--           ((.) * * *
--                (\ rev ds ->
--                   case ds of wild *
--                     [] -> [] *
--                     (:) x xs -> (++) * (rev xs) ((:) * x ([] *)))
--                (\ eta -> (\ g -> (.) * * * (absH *) g) eta))
--     worker = fix * g
-- in (\ g -> (.) * * * (absH *) g) worker

repeat (any-call (unfold '.)) ; smash

-- let worker =
--       fix *
--           (\ x x ->
--              repH *
--                   (case x of wild *
--                      [] -> [] *
--                      (:) x xs -> (++) * (absH * (x xs)) ((:) * x ([] *))))
-- in \ x -> absH * (worker x)

one-td (case-float-arg-lemma repHstrict)

-- Goal:
-- forall *. repH * (undefined *) = undefined *

lhs unfold

-- Goal:
-- forall *. (++) * (undefined *) = undefined *

lhs (one-td (unfold-rule appendFix))

-- Goal:
-- forall *. myAppend * (undefined *) = undefined *

lhs unfold

-- Goal:
-- forall *.
-- \ ys ->
--   case undefined * of wild *
--     [] -> ys
--     (:) x xs -> (:) * x (myAppend * xs ys)
-- =
-- undefined *

both (innermost undefined-expr)

-- Goal:
-- forall *. undefined * = undefined *

end-proof -- proven repHstrict

-- let worker =
--       fix *
--           (\ x x ->
--              case x of wild *
--                [] -> repH * ([] *)
--                (:) x xs -> repH * ((++) * (absH * (x xs)) ((:) * x ([] *))))
-- in \ x -> absH * (worker x)

one-td (lemma-forward "repH ++")

-- let worker =
--       fix *
--           (\ x x ->
--              case x of wild *
--                [] -> repH * ([] *)
--                (:) x xs -> (.) * * * (repH * (absH * (x xs))) (repH * ((:) * x ([] *))))
-- in \ x -> absH * (worker x)

repeat (any-call (unfold '.))

-- let worker =
--       fix *
--           (\ x x ->
--              case x of wild *
--                [] -> repH * ([] *)
--                (:) x xs -> \ x -> repH * (absH * (x xs)) (repH * ((:) * x ([] *)) x))
-- in \ x -> absH * (worker x)

one-td (unfold-rule repH-absH-fusion)

-- Goal:
-- forall * h. repH * (absH * h) = h

assume -- proven repH-absH-fusion

-- let worker =
--       fix *
--           (\ x x ->
--              case x of wild *
--                [] -> repH * ([] *)
--                (:) x xs -> \ x -> x xs (repH * ((:) * x ([] *)) x))
-- in \ x -> absH * (worker x)

one-td (lemma-forward "repH (:)")

-- let worker =
--       fix *
--           (\ x x ->
--              case x of wild *
--                [] -> repH * ([] *)
--                (:) x xs -> \ x -> x xs ((.) * * * ((:) * x) (repH * ([] *)) x))
-- in \ x -> absH * (worker x)

any-td (lemma-forward "repH []")

-- let worker =
--       fix *
--           (\ x x ->
--              case x of wild *
--                [] -> id *
--                (:) x xs -> \ x -> x xs ((.) * * * ((:) * x) (id *) x))
-- in \ x -> absH * (worker x)

any-call (unfold 'fix)

-- let worker =
--       let rec x =
--                 (\ x x ->
--                    case x of wild *
--                      [] -> id *
--                      (:) x xs -> \ x -> x xs ((.) * * * ((:) * x) (id *) x)) x
--       in x
-- in \ x -> absH * (worker x)

any-call (unfold 'absH)

-- let worker =
--       let rec x =
--                 (\ x x ->
--                    case x of wild *
--                      [] -> id *
--                      (:) x xs -> \ x -> x xs ((.) * * * ((:) * x) (id *) x)) x
--       in x
-- in \ x -> worker x ([] *)

bash

-- let rec x = \ x ->
--           case x of wild *
--             [] -> \ x -> x
--             (:) x xs -> \ x -> x xs ((:) * x x)
-- in \ x -> x x ([] *)

unshadow

-- let rec x = \ x0 ->
--           case x0 of wild *
--             [] -> \ x1 -> x1
--             (:) x1 xs -> \ x2 -> x xs ((:) * x1 x2)
-- in \ x0 -> x x0 ([] *)