simp [Array.getElem_set, hmark, h]
case extension
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
idx : Nat
hidx : idx < aig.decls.size
hmark : cache1.marks[idx] = true
⊢ cache2.marks[idx] = true
no goals