match heval1:(go aig start h1 (State.empty aig)).val.cnf.eval assign with
| true =>
  have heval2 := (go aig start h1 (.empty aig)).val.cache.inv.heval
  specialize heval2 assign heval1 start h1 go_marked
  simp [h] at heval2
  simp [heval2]
| false =>
  simp [heval1]
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
⊢ CNF.eval assign ([(Sum.inr ⟨start, h1⟩, true)] :: (go aig start h1 (State.empty aig)).val.cnf) = false
no goals