Theorem: conNotSelfContainL (Bml/Tableau.lean)

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

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