constructor
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ (∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ) ↔
    ∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
case mp
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ (∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ) →
    ∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ

case mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ (∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ) →
    ∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ