Theorem: LoVe.Odd_1 (LoVe/Labs/Lab5Solution.lean)

State before:
⊢ Odd 1
Tactic:
intro ho1
State after:
ho1 : Even 1
⊢ False

State before:
ho1 : Even 1
⊢ False
Tactic:
cases ho1
State after:
no goals