apply IsExtensionBy.mk
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
⊢ cache1.IsExtensionBy cache2 idx ⋯
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_1 : Nat) (hidx : idx_1 < aig.decls.size), cache1.marks[idx_1] = true → cache2.marks[idx_1] = true

case trueAt
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
⊢ cache2.marks[idx] = true