. intros
  apply (go aig expr).property
case hprefix.size_le
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
start : Nat
hstart : start < aig.decls.size
⊢ { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls.size ≤ (go aig expr).val.aig.decls.size
no goals