omega
aig : AIG Nat
cnf1 cnf2 : CNF aig.CNFVar
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
idx : Nat
hbound : idx < cache1.marks.size
h : cache2.marks = cache1.marks.set ⟨idx, hbound⟩ true
this : cache1.marks.size = aig.decls.size
⊢ idx < aig.decls.size
no goals