exact h23
case h23
aig : AIG Nat
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
state1 state2 state3 : State aig
h12 : state1.IsExtensionBy state2 new1 hnew1
h23 : state2.IsExtensionBy state3 new2 hnew2
⊢ state2.cache.IsExtensionBy state3.cache ?new2 ?hnew2
no goals