Theorem: Cpdt.Chapter3.OddList.olength_oCons (Cpdt/Chapter3/Mutual.lean)

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