apply eq_of_heq
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ (a :: as).append bs = a :: as.append bs
case h
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ (a :: as).append bs ≅ a :: as.append bs