dsimp
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
start : Nat
hstart : start < aig.decls.size
⊢ ⟦{
        aig :=
          (let res := mkFullAdderOut aig input;
            let aig_1 := res.aig;
            let outRef := res.ref;
            let_fun haig1 := ⋯;
            let input_1 := input.cast haig1;
            let res_1 := mkFullAdderCarry aig_1 input_1;
            let aig_2 := res_1.aig;
            let carryRef := res_1.ref;
            let_fun haig2 := ⋯;
            let outRef := outRef.cast haig2;
            let_fun hle := ⋯;
            { aig := aig_2, out := outRef, cout := carryRef, hle := hle }).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 := (mkFullAdderCarry (mkFullAdderOut aig input).aig (input.cast ⋯)).aig,
        ref := { gate := start, hgate := ⋯ } },
      assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧