rw [HList.cons_append]
case h
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ (HList.cons a as).append bs ≅ HList.cons a (⋯ ▸ HList.append as bs)
case h
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ HList.cons a (HList.append as bs) ≅ HList.cons a (⋯ ▸ HList.append as bs)