apply HList.cons_hcongr
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)
case h.a
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ α = α

case h.a
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ List.replicate n α ++ List.replicate m α = List.replicate (m + n) α

case h.a
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ a ≅ a

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