elim_casts
case h.a
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ HList.append as bs ≅ ⋯ ▸ HList.append as bs
case h.a
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ HList.append as bs ≅ HList.append as bs