. intro h assign
  apply toCNF.denote_as_go
  specialize h (toCNF.projectLeftAssign assign)
  assumption
case mpr
entry : Entrypoint Nat
⊢ entry.unsat →
    CNF.unsat
      ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
no goals