Theorem: notnot_notSelfContain (Bml/Tableau.lean)

State before:
φ : Formula
⊢ ~~φ ≠ φ
Tactic:
intro hyp
State after:
φ : Formula
hyp : ~~φ = φ
⊢ False

State before:
φ : Formula
hyp : ~~φ = φ
⊢ False
Tactic:
cases hyp
State after:
no goals