Theorem: conNotSelfContainR (Bml/Tableau.lean)

State before:
φ1 φ2 : Formula
⊢ φ1⋀φ2 ≠ φ2
Tactic:
intro hyp
State after:
φ1 φ2 : Formula
hyp : φ1⋀φ2 = φ2
⊢ False

State before:
φ1 φ2 : Formula
hyp : φ1⋀φ2 = φ2
⊢ False
Tactic:
cases hyp
State after:
no goals