rw [LList.cons_append, LList.cons_append, LList.cons_append]
case cons
α : Sort u_1
l m n : Nat
bs : LList α m
cs : LList α n
n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : (as✝.append bs).append cs ≅ as✝.append (bs.append cs)
⊢ ((a✝ :: as✝).append bs).append cs ≅ (a✝ :: as✝).append (bs.append cs)
case cons
α : Sort u_1
l m n : Nat
bs : LList α m
cs : LList α n
n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : (as✝.append bs).append cs ≅ as✝.append (bs.append cs)
⊢ a✝ :: (as✝.append bs).append cs ≅ a✝ :: as✝.append (bs.append cs)