Theorem: Cpdt.Chapter3.elength_eappend (Cpdt/Chapter3/Mutual.lean)

State before:
xs ys : EvenList
⊢ elength (eappend xs ys) = elength xs + elength ys
Tactic:
apply @EvenList.rec
  (fun xs => ∀ ys, elength (eappend xs ys) = elength xs + elength ys)
  (fun ol => ∀ el, olength (oappend ol el) = olength ol + elength el)
<;> simp_all[Nat.add_assoc]
State after:
no goals