simp at hmark
aig : AIG Nat
assign : aig.CNFVar → Bool
_heval✝ : CNF.eval assign [] = true
idx : Nat
hbound : idx < aig.decls.size
hmark : (mkArray aig.decls.size false)[idx] = true
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hbound } }, projectLeftAssign assign⟧ =
    projectRightAssign assign idx hbound
no goals