simp only [TernaryInput.cast, Ref_cast', id_eq, Int.reduceNeg, denote_mkOrCached,
  denote_projected_entry, denote_mkAndCached, denote_mkNotCached]
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦let res := aig.mkAndCached { lhs := input.discr, rhs := input.lhs };
      let aig_1 := res.aig;
      let lhsRef := res.ref;
      let input_1 := input.cast ⋯;
      let res_1 := aig_1.mkNotCached input_1.discr;
      let aig_2 := res_1.aig;
      let notDiscr := res_1.ref;
      let input_2 := input_1.cast ⋯;
      let res_2 := aig_2.mkAndCached { lhs := notDiscr, rhs := input_2.rhs };
      let aig_3 := res_2.aig;
      let rhsRef := res_2.ref;
      let lhsRef := lhsRef.cast ⋯;
      aig_3.mkOrCached { lhs := lhsRef, rhs := rhsRef },
      assign⟧ =
    (⟦{ aig := aig, ref := input.discr }, assign⟧ && ⟦{ aig := aig, ref := input.lhs }, assign⟧ ||
      !⟦{ aig := aig, ref := input.discr }, assign⟧ && ⟦{ aig := aig, ref := input.rhs }, assign⟧)
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ (⟦{
          aig :=
            (((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
                      { gate := input.discr.gate, hgate := ⋯ }).aig.mkAndCached
                {
                  lhs :=
                    ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
                        { gate := input.discr.gate, hgate := ⋯ }).ref,
                  rhs := { gate := input.rhs.gate, hgate := ⋯ } }).aig,
          ref := { gate := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.gate, hgate := ⋯ } },
        assign⟧ ||
      !⟦{ aig := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig,
              ref := { gate := input.discr.gate, hgate := ⋯ } },
            assign⟧ &&
        ⟦{
            aig :=
              ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
                  { gate := input.discr.gate, hgate := ⋯ }).aig,
            ref := { gate := input.rhs.gate, hgate := ⋯ } },
          assign⟧) =
    (⟦{ aig := aig, ref := input.discr }, assign⟧ && ⟦{ aig := aig, ref := input.lhs }, assign⟧ ||
      !⟦{ aig := aig, ref := input.discr }, assign⟧ && ⟦{ aig := aig, ref := input.rhs }, assign⟧)