Theorem: Cpdt.Chapter3.EvenList.elength_econs (Cpdt/Chapter3/Mutual.lean)

State before:
x : Nat
xs : OddList
⊢ elength (eCons x xs) = 1 + olength xs
Tactic:
rw[elength]
State after:
no goals