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

State before:
⊢ elength nil = 0
Tactic:
rfl
State after:
no goals