constructor
case h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
⊢ σ' ∘ State.withTemps.vMap s.toState =
      PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ∘
        State.withTemps.vMap s.toState ∧
    PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ⊨
      Cnf.toPropFun s.cnf
case h.left
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
⊢ σ' ∘ State.withTemps.vMap s.toState =
    PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ∘
      State.withTemps.vMap s.toState

case h.right
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
⊢ PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ⊨
    Cnf.toPropFun s.cnf