Theorem: LeanSAT.Model.PropFun.semVars_impl (LeanSAT/Model/PropVars.lean)

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₁ ⇨ φ₂) ⊆ semVars φ₁ ∪ semVars φ₂
Tactic:
rw [himp_eq]
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₂ ⊔ φ₁ᶜ) ⊆ semVars φ₁ ∪ semVars φ₂

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₂ ⊔ φ₁ᶜ) ⊆ semVars φ₁ ∪ semVars φ₂
Tactic:
have := semVars_disj (φ₁ᶜ) φ₂
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
this : semVars (φ₁ᶜ ⊔ φ₂) ⊆ semVars φ₁ᶜ ∪ semVars φ₂
⊢ semVars (φ₂ ⊔ φ₁ᶜ) ⊆ semVars φ₁ ∪ semVars φ₂

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
this : semVars (φ₁ᶜ ⊔ φ₂) ⊆ semVars φ₁ᶜ ∪ semVars φ₂
⊢ semVars (φ₂ ⊔ φ₁ᶜ) ⊆ semVars φ₁ ∪ semVars φ₂
Tactic:
rw [sup_comm, semVars_neg] at this
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
this : semVars (φ₂ ⊔ φ₁ᶜ) ⊆ semVars φ₁ ∪ semVars φ₂
⊢ semVars (φ₂ ⊔ φ₁ᶜ) ⊆ semVars φ₁ ∪ semVars φ₂

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
this : semVars (φ₂ ⊔ φ₁ᶜ) ⊆ semVars φ₁ ∪ semVars φ₂
⊢ semVars (φ₂ ⊔ φ₁ᶜ) ⊆ semVars φ₁ ∪ semVars φ₂
Tactic:
exact this
State after:
no goals