case h
α : Type u
β : Type v
γ : Type w
⊢ ∀ (x : Type u_1), List.append = appendTR
α : Type u
β : Type v
γ : Type w
⊢ @List.append = @appendTR
apply funext
case h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
⊢ List.append = appendTR
case h
α : Type u
β : Type v
γ : Type w
⊢ ∀ (x : Type u_1), List.append = appendTR
intro α
case h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
⊢ ∀ (x : List α), List.append x = appendTR x
case h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
⊢ List.append = appendTR
apply funext
case h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
as : List α
⊢ List.append as = appendTR as
case h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
⊢ ∀ (x : List α), List.append x = appendTR x
intro as
case h.h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
as : List α
⊢ ∀ (x : List α), List.append as x = appendTR as x
case h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
as : List α
⊢ List.append as = appendTR as
apply funext
case h.h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
as bs : List α
⊢ List.append as bs = appendTR as bs
case h.h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
as : List α
⊢ ∀ (x : List α), List.append as x = appendTR as x
intro bs
case h.h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
as bs : List α
⊢ List.append as bs = reverseAux (reverseAux as nil) bs
case h.h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
as bs : List α
⊢ List.append as bs = appendTR as bs
simp [appendTR, reverse]
no goals
case h.h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
as bs : List α
⊢ List.append as bs = reverseAux (reverseAux as nil) bs
induction as with
| nil  => rfl
| cons a as ih =>
  simp [reverseAux, List.append, ih, reverseAux_reverseAux]
no goals
case h.h.h.nil
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
bs : List α
⊢ List.append nil bs = reverseAux (reverseAux nil nil) bs
rfl
no goals
case h.h.h.cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
bs : List α
a : α
as : List α
ih : List.append as bs = reverseAux (reverseAux as nil) bs
⊢ List.append (a :: as) bs = reverseAux (reverseAux (a :: as) nil) bs
simp [reverseAux, List.append, ih, reverseAux_reverseAux]