Theorem: modus_tollens (Test/Bool/ModusTollens.lean)

State before:
p q : Bool
⊢ (!q) = true → (p = true → q = true) → (!p) = true
Tactic:
intro hnq hpq
State after:
p q : Bool
hnq : (!q) = true
hpq : p = true → q = true
⊢ (!p) = true

State before:
p q : Bool
hnq : (!q) = true
hpq : p = true → q = true
⊢ (!p) = true
Tactic:
cases p <;> simp_all
State after:
no goals