intro σ
case h.a.h
L : Type ?u.23742
ν : Type u_1
inst✝ : LitVar L ν
C : Clause (Literal ν)
s : LawfulState ν
τ : PropAssignment ν
⊢ ∀ (a : PropAssignment IVar),
    τ = PropAssignment.map s.1.vMap a ∧
        a ⊨ Cnf.toPropFun s.1.cnf ∧
          (PropAssignment.map s.1.vMap a ⊨ Clause.toPropFun s.1.assumeVars ∨
            PropAssignment.map s.1.vMap a ⊨ Clause.toPropFun C) ↔
      (τ = PropAssignment.map s.vMap a ∧ a ⊨ Cnf.toPropFun s.cnf) ∧
        (τ ⊨ Clause.toPropFun s.assumeVars ∨ τ ⊨ Clause.toPropFun C)
case h.a.h
L : Type ?u.23742
ν : Type u_1
inst✝ : LitVar L ν
C : Clause (Literal ν)
s : LawfulState ν
τ : PropAssignment ν
σ : PropAssignment IVar
⊢ τ = 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)