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]
xs ys : EvenList
⊢ elength (eappend xs ys) = elength xs + elength ys
no goals