case h
α : Type u
β : Type v
γ : Type w
⊢ ∀ (x : Type u_1), length = lengthTR
α : Type u
β : Type v
γ : Type w
⊢ @length = @lengthTR
apply funext
case h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
⊢ length = lengthTR
case h
α : Type u
β : Type v
γ : Type w
⊢ ∀ (x : Type u_1), length = lengthTR
intro α
case h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
⊢ ∀ (x : List α), length x = lengthTR x
case h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
⊢ length = lengthTR
apply funext
case h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
as : List α
⊢ length as = lengthTR as
case h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
⊢ ∀ (x : List α), length x = lengthTR x
intro as
no goals
case h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
as : List α
⊢ length as = lengthTR as
simp [lengthTR, ← length_add_eq_lengthTRAux]