apply Cache.IsExtensionBy_rfl <;> assumption
aig : AIG Nat
idx : Nat
omega : idx < aig.decls.size
state : State aig
h : idx < state.cache.marks.size
hmarked : state.cache.marks[idx] = true
⊢ state.IsExtensionBy state idx ⋯
no goals