rw [← exists_and_right]
case h.a
L : Type ?u.23742
ν : Type u_1
inst✝ : LitVar L ν
C : Clause (Literal ν)
s : LawfulState ν
τ : PropAssignment ν
⊢ (∃ σ,
      τ = PropAssignment.map s.1.vMap σ ∧
        σ ⊨ Cnf.toPropFun s.1.cnf ∧
          (PropAssignment.map s.1.vMap σ ⊨ Clause.toPropFun s.1.assumeVars ∨
            PropAssignment.map s.1.vMap σ ⊨ Clause.toPropFun C)) ↔
    (∃ σ, τ = PropAssignment.map s.vMap σ ∧ σ ⊨ Cnf.toPropFun s.cnf) ∧
      (τ ⊨ Clause.toPropFun s.assumeVars ∨ τ ⊨ Clause.toPropFun C)
case h.a
L : Type ?u.23742
ν : Type u_1
inst✝ : LitVar L ν
C : Clause (Literal ν)
s : LawfulState ν
τ : PropAssignment ν
⊢ (∃ σ,
      τ = PropAssignment.map s.1.vMap σ ∧
        σ ⊨ Cnf.toPropFun s.1.cnf ∧
          (PropAssignment.map s.1.vMap σ ⊨ Clause.toPropFun s.1.assumeVars ∨
            PropAssignment.map s.1.vMap σ ⊨ Clause.toPropFun C)) ↔
    ∃ x,
      (τ = PropAssignment.map s.vMap x ∧ x ⊨ Cnf.toPropFun s.cnf) ∧
        (τ ⊨ Clause.toPropFun s.assumeVars ∨ τ ⊨ Clause.toPropFun C)