Theorem: Cpdt.Chapter4.IsZero_contra (Cpdt/Chapter4/InductivePred.lean)

State before:
⊢ IsZero 1 → False
Tactic:
intro h
State after:
h : IsZero 1
⊢ False

State before:
h : IsZero 1
⊢ False
Tactic:
cases h
State after:
no goals