. exact hmarked
case trueAt
aig : AIG Nat
cnf : CNF aig.CNFVar
idx : Nat
omega : idx < aig.decls.size
cache : Cache aig cnf
h : idx < cache.marks.size
hmarked : cache.marks[idx] = true
⊢ cache.marks[idx] = true
no goals