Theorem: AIG.toCNF.State.IsExtensionBy_rfl (LeanSAT/AIG/CNF.lean)

State before:
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 ⋯
Tactic:
apply Cache.IsExtensionBy_rfl <;> assumption
State after:
no goals