Theorem: four_is_not_three (Fpil/Chap10/Sec03.lean)

State before:
⊢ ¬IsThree 4
Tactic:
simp [Not]
State after:
⊢ IsThree 4 → False

State before:
⊢ IsThree 4 → False
Tactic:
intro h
State after:
h : IsThree 4
⊢ False

State before:
h : IsThree 4
⊢ False
Tactic:
cases h
State after:
no goals