Theorem: LeanSAT.Model.PropForm.agreeOn_vars (LeanSAT/Model/PropVars.lean)

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁ σ₂ : PropAssignment ν
⊢ PropAssignment.agreeOn (↑(vars φ)) σ₁ σ₂ → (σ₁ ⊨ φ ↔ σ₂ ⊨ φ)
Tactic:
intro h
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(vars φ)) σ₁ σ₂
⊢ σ₁ ⊨ φ ↔ σ₂ ⊨ φ

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(vars φ)) σ₁ σ₂
⊢ σ₁ ⊨ φ ↔ σ₂ ⊨ φ
Tactic:
simp [SemanticEntails.entails, satisfies, eval_of_agreeOn_vars h]
State after:
no goals