rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)]
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ ⟦{ aig := (mkFullAdderCarry (mkFullAdderOut aig input).aig (input.cast ⋯)).aig,
        ref := { gate := start, hgate := ⋯ } },
      assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ ⟦{ aig := (mkFullAdderOut aig input).aig, ref := { gate := start, hgate := ?m.7385 } }, assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧

α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ start < (mkFullAdderOut aig input).aig.decls.size