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

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

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
σ₁ σ₂ : PropAssignment ν
h : PropAssignment.agreeOn (↑(vars φ)) σ₁ σ₂
⊢ eval σ₁ φ = eval σ₂ φ
Tactic:
induction φ <;> simp_all [PropAssignment.agreeOn, eval, vars]
State after:
no goals