apply LList.cons_hcongr
case cons
α : Sort u_1
n n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : as✝.append LList.nil ≅ as✝
⊢ a✝ :: as✝.append LList.nil ≅ a✝ :: as✝
case cons.a
α : Sort u_1
n n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : as✝.append LList.nil ≅ as✝
⊢ α = α

case cons.a
α : Sort u_1
n n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : as✝.append LList.nil ≅ as✝
⊢ 0 + n✝ = n✝

case cons.a
α : Sort u_1
n n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : as✝.append LList.nil ≅ as✝
⊢ a✝ ≅ a✝

case cons.a
α : Sort u_1
n n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : as✝.append LList.nil ≅ as✝
⊢ as✝.append LList.nil ≅ as✝