Theorem: LeanColls.Seq.size_append (LeanColls/Classes/Seq.lean)

State before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
c1 c2 : C
⊢ size (c1 ++ c2) = size c1 + size c2
Tactic:
simp [size_def]
State after:
no goals