have heval2 := (go aig start h1 (.empty aig)).val.cache.inv.heval
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign : aig.CNFVar → Bool
h : ⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, projectLeftAssign assign⟧ = false
heval1 : CNF.eval assign (go aig start h1 (State.empty aig)).val.cnf = true
⊢ CNF.eval assign ([(Sum.inr ⟨start, h1⟩, true)] :: (go aig start h1 (State.empty aig)).val.cnf) = false
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign : aig.CNFVar → Bool
h : ⟦{ aig := aig, ref := { gate := start, hgate := h1 } }, projectLeftAssign assign⟧ = false
heval1 : CNF.eval assign (go aig start h1 (State.empty aig)).val.cnf = true
heval2 :
  ∀ (assign : aig.CNFVar → Bool),
    CNF.eval assign (go aig start h1 (State.empty aig)).val.cnf = true →
      ∀ (idx : Nat) (hbound : idx < aig.decls.size),
        (go aig start h1 (State.empty aig)).val.cache.marks[idx] = true →
          ⟦{ aig := aig, ref := { gate := idx, hgate := hbound } }, projectLeftAssign assign⟧ =
            projectRightAssign assign idx hbound
⊢ CNF.eval assign ([(Sum.inr ⟨start, h1⟩, true)] :: (go aig start h1 (State.empty aig)).val.cnf) = false