-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Udiv.lean
theorem blastDivSubtractShift_decl_eq (aig : AIG α) (falseRef trueRef : AIG.Ref aig)
     (n d : AIG.RefVec aig w) (wn wr : Nat) (q r : AIG.RefVec aig w) :
    ∀ (idx : Nat) (h1) (h2),
        (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig.decls[idx]'h2 = aig.decls[idx]'h1

Proof state:
case h2
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
falseRef trueRef : aig.Ref
n d : aig.RefVec w
wn wr : Nat
q r : aig.RefVec w
res : BlastDivSubtractShiftOutput aig w
hres :
  {
      aig :=
        (AIG.RefVec.ite
            (AIG.RefVec.ite
                (BVPred.mkUlt
                    (blastSub
                        (blastShiftConcat
                            (blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                            { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                        {
                          lhs :=
                            ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯,
                          rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                    {
                      lhs :=
                        (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯).cast
                          ⋯,
                      rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).aig
                {
                  discr :=
                    (BVPred.mkUlt
                        (blastSub
                            (blastShiftConcat
                                (blastShiftConcat
                                    (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                    { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                            {
                              lhs :=
                                ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                  ⋯,
                              rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                        {
                          lhs :=
                            (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                  ⋯).cast
                              ⋯,
                          rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).ref,
                  lhs :=
                    (((blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                    { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).vec.cast
                              ⋯).cast
                          ⋯).cast
                      ⋯,
                  rhs :=
                    ((blastShiftConcat
                                (blastShiftConcat
                                    (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                    { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).vec.cast
                          ⋯).cast
                      ⋯ }).aig
            {
              discr :=
                (BVPred.mkUlt
                        (blastSub
                            (blastShiftConcat
                                (blastShiftConcat
                                    (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                    { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                            {
                              lhs :=
                                ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                  ⋯,
                              rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                        {
                          lhs :=
                            (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                  ⋯).cast
                              ⋯,
                          rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).ref.cast
                  ⋯,
              lhs :=
                (((((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯).cast
                          ⋯).cast
                      ⋯).cast
                  ⋯,
              rhs :=
                ((blastSub
                            (blastShiftConcat
                                (blastShiftConcat
                                    (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                    { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                            {
                              lhs :=
                                ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                  ⋯,
                              rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).vec.cast
                      ⋯).cast
                  ⋯ }).aig,
      wn := wn - 1, wr := wr + 1,
      q :=
        (AIG.RefVec.ite
                (BVPred.mkUlt
                    (blastSub
                        (blastShiftConcat
                            (blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                            { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                        {
                          lhs :=
                            ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯,
                          rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                    {
                      lhs :=
                        (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯).cast
                          ⋯,
                      rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).aig
                {
                  discr :=
                    (BVPred.mkUlt
                        (blastSub
                            (blastShiftConcat
                                (blastShiftConcat
                                    (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                    { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                            {
                              lhs :=
                                ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                  ⋯,
                              rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                        {
                          lhs :=
                            (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                  ⋯).cast
                              ⋯,
                          rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).ref,
                  lhs :=
                    (((blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                    { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).vec.cast
                              ⋯).cast
                          ⋯).cast
                      ⋯,
                  rhs :=
                    ((blastShiftConcat
                                (blastShiftConcat
                                    (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                    { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).vec.cast
                          ⋯).cast
                      ⋯ }).vec.cast
          ⋯,
      r :=
        (AIG.RefVec.ite
            (AIG.RefVec.ite
                (BVPred.mkUlt
                    (blastSub
                        (blastShiftConcat
                            (blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                            { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                        {
                          lhs :=
                            ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯,
                          rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                    {
                      lhs :=
                        (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯).cast
                          ⋯,
                      rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).aig
                {
                  discr :=
                    (BVPred.mkUlt
                        (blastSub
                            (blastShiftConcat
                                (blastShiftConcat
                                    (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                    { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                            {
                              lhs :=
                                ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                  ⋯,
                              rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                        {
                          lhs :=
                            (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                  ⋯).cast
                              ⋯,
                          rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).ref,
                  lhs :=
                    (((blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                    { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).vec.cast
                              ⋯).cast
                          ⋯).cast
                      ⋯,
                  rhs :=
                    ((blastShiftConcat
                                (blastShiftConcat
                                    (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                    { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).vec.cast
                          ⋯).cast
                      ⋯ }).aig
            {
              discr :=
                (BVPred.mkUlt
                        (blastSub
                            (blastShiftConcat
                                (blastShiftConcat
                                    (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                    { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                            {
                              lhs :=
                                ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                  ⋯,
                              rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                        {
                          lhs :=
                            (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                  ⋯).cast
                              ⋯,
                          rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).ref.cast
                  ⋯,
              lhs :=
                (((((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯).cast
                          ⋯).cast
                      ⋯).cast
                  ⋯,
              rhs :=
                ((blastSub
                            (blastShiftConcat
                                (blastShiftConcat
                                    (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                    { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                            {
                              lhs :=
                                ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                  ⋯,
                              rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).vec.cast
                      ⋯).cast
                  ⋯ }).vec,
      hle := ⋯ } =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    {
            aig :=
              (AIG.RefVec.ite
                  (AIG.RefVec.ite
                      (BVPred.mkUlt
                          (blastSub
                              (blastShiftConcat
                                  (blastShiftConcat
                                      (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                      { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                  { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                              {
                                lhs :=
                                  ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                    ⋯,
                                rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                          {
                            lhs :=
                              (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                    ⋯).cast
                                ⋯,
                            rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).aig
                      {
                        discr :=
                          (BVPred.mkUlt
                              (blastSub
                                  (blastShiftConcat
                                      (blastShiftConcat
                                          (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                          { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                      { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                                  {
                                    lhs :=
                                      ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast
                                            ⋯).cast
                                        ⋯,
                                    rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                              {
                                lhs :=
                                  (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast
                                            ⋯).cast
                                        ⋯).cast
                                    ⋯,
                                rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).ref,
                        lhs :=
                          (((blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                          { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).vec.cast
                                    ⋯).cast
                                ⋯).cast
                            ⋯,
                        rhs :=
                          ((blastShiftConcat
                                      (blastShiftConcat
                                          (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                          { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                      { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).vec.cast
                                ⋯).cast
                            ⋯ }).aig
                  {
                    discr :=
                      (BVPred.mkUlt
                              (blastSub
                                  (blastShiftConcat
                                      (blastShiftConcat
                                          (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                          { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                      { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                                  {
                                    lhs :=
                                      ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast
                                            ⋯).cast
                                        ⋯,
                                    rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                              {
                                lhs :=
                                  (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast
                                            ⋯).cast
                                        ⋯).cast
                                    ⋯,
                                rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).ref.cast
                        ⋯,
                    lhs :=
                      (((((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯).cast
                                ⋯).cast
                            ⋯).cast
                        ⋯,
                    rhs :=
                      ((blastSub
                                  (blastShiftConcat
                                      (blastShiftConcat
                                          (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                          { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                      { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                                  {
                                    lhs :=
                                      ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast
                                            ⋯).cast
                                        ⋯,
                                    rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).vec.cast
                            ⋯).cast
                        ⋯ }).aig,
            wn := wn - 1, wr := wr + 1,
            q :=
              (AIG.RefVec.ite
                      (BVPred.mkUlt
                          (blastSub
                              (blastShiftConcat
                                  (blastShiftConcat
                                      (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                      { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                  { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                              {
                                lhs :=
                                  ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                    ⋯,
                                rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                          {
                            lhs :=
                              (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                    ⋯).cast
                                ⋯,
                            rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).aig
                      {
                        discr :=
                          (BVPred.mkUlt
                              (blastSub
                                  (blastShiftConcat
                                      (blastShiftConcat
                                          (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                          { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                      { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                                  {
                                    lhs :=
                                      ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast
                                            ⋯).cast
                                        ⋯,
                                    rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                              {
                                lhs :=
                                  (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast
                                            ⋯).cast
                                        ⋯).cast
                                    ⋯,
                                rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).ref,
                        lhs :=
                          (((blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                          { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).vec.cast
                                    ⋯).cast
                                ⋯).cast
                            ⋯,
                        rhs :=
                          ((blastShiftConcat
                                      (blastShiftConcat
                                          (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                          { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                      { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).vec.cast
                                ⋯).cast
                            ⋯ }).vec.cast
                ⋯,
            r :=
              (AIG.RefVec.ite
                  (AIG.RefVec.ite
                      (BVPred.mkUlt
                          (blastSub
                              (blastShiftConcat
                                  (blastShiftConcat
                                      (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                      { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                  { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                              {
                                lhs :=
                                  ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                    ⋯,
                                rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                          {
                            lhs :=
                              (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                    ⋯).cast
                                ⋯,
                            rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).aig
                      {
                        discr :=
                          (BVPred.mkUlt
                              (blastSub
                                  (blastShiftConcat
                                      (blastShiftConcat
                                          (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                          { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                      { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                                  {
                                    lhs :=
                                      ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast
                                            ⋯).cast
                                        ⋯,
                                    rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                              {
                                lhs :=
                                  (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast
                                            ⋯).cast
                                        ⋯).cast
                                    ⋯,
                                rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).ref,
                        lhs :=
                          (((blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                          { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).vec.cast
                                    ⋯).cast
                                ⋯).cast
                            ⋯,
                        rhs :=
                          ((blastShiftConcat
                                      (blastShiftConcat
                                          (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                          { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                      { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).vec.cast
                                ⋯).cast
                            ⋯ }).aig
                  {
                    discr :=
                      (BVPred.mkUlt
                              (blastSub
                                  (blastShiftConcat
                                      (blastShiftConcat
                                          (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                          { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                      { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                                  {
                                    lhs :=
                                      ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast
                                            ⋯).cast
                                        ⋯,
                                    rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                              {
                                lhs :=
                                  (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast
                                            ⋯).cast
                                        ⋯).cast
                                    ⋯,
                                rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).ref.cast
                        ⋯,
                    lhs :=
                      (((((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯).cast
                                ⋯).cast
                            ⋯).cast
                        ⋯,
                    rhs :=
                      ((blastSub
                                  (blastShiftConcat
                                      (blastShiftConcat
                                          (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                          { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                      { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                                  {
                                    lhs :=
                                      ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast
                                            ⋯).cast
                                        ⋯,
                                    rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).vec.cast
                            ⋯).cast
                        ⋯ }).vec,
            hle := ⋯ }.aig.decls.size
⊢ idx✝ <
    (BVPred.mkUlt
            (blastSub
                (blastShiftConcat
                    (blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                        { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                    { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                { lhs := ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯,
                  rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
            { lhs := (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯).cast ⋯,
              rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).aig.decls.size

Tactic:
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := BVPred.mkUlt)

Result:
case h2.h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
falseRef trueRef : aig.Ref
n d : aig.RefVec w
wn wr : Nat
q r : aig.RefVec w
res : BlastDivSubtractShiftOutput aig w
hres :
  {
      aig :=
        (AIG.RefVec.ite
            (AIG.RefVec.ite
                (BVPred.mkUlt
                    (blastSub
                        (blastShiftConcat
                            (blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                            { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                        {
                          lhs :=
                            ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯,
                          rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                    {
                      lhs :=
                        (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯).cast
                          ⋯,
                      rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).aig
                {
                  discr :=
                    (BVPred.mkUlt
                        (blastSub
                            (blastShiftConcat
                                (blastShiftConcat
                                    (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                    { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                            {
                              lhs :=
                                ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                  ⋯,
                              rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                        {
                          lhs :=
                            (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                  ⋯).cast
                              ⋯,
                          rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).ref,
                  lhs :=
                    (((blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                    { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).vec.cast
                              ⋯).cast
                          ⋯).cast
                      ⋯,
                  rhs :=
                    ((blastShiftConcat
                                (blastShiftConcat
                                    (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                    { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).vec.cast
                          ⋯).cast
                      ⋯ }).aig
            {
              discr :=
                (BVPred.mkUlt
                        (blastSub
                            (blastShiftConcat
                                (blastShiftConcat
                                    (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                    { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                            {
                              lhs :=
                                ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                  ⋯,
                              rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                        {
                          lhs :=
                            (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                  ⋯).cast
                              ⋯,
                          rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).ref.cast
                  ⋯,
              lhs :=
                (((((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯).cast
                          ⋯).cast
                      ⋯).cast
                  ⋯,
              rhs :=
                ((blastSub
                            (blastShiftConcat
                                (blastShiftConcat
                                    (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                    { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                            {
                              lhs :=
                                ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                  ⋯,
                              rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).vec.cast
                      ⋯).cast
                  ⋯ }).aig,
      wn := wn - 1, wr := wr + 1,
      q :=
        (AIG.RefVec.ite
                (BVPred.mkUlt
                    (blastSub
                        (blastShiftConcat
                            (blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                            { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                        {
                          lhs :=
                            ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯,
                          rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                    {
                      lhs :=
                        (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯).cast
                          ⋯,
                      rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).aig
                {
                  discr :=
                    (BVPred.mkUlt
                        (blastSub
                            (blastShiftConcat
                                (blastShiftConcat
                                    (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                    { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                            {
                              lhs :=
                                ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                  ⋯,
                              rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                        {
                          lhs :=
                            (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                  ⋯).cast
                              ⋯,
                          rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).ref,
                  lhs :=
                    (((blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                    { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).vec.cast
                              ⋯).cast
                          ⋯).cast
                      ⋯,
                  rhs :=
                    ((blastShiftConcat
                                (blastShiftConcat
                                    (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                    { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).vec.cast
                          ⋯).cast
                      ⋯ }).vec.cast
          ⋯,
      r :=
        (AIG.RefVec.ite
            (AIG.RefVec.ite
                (BVPred.mkUlt
                    (blastSub
                        (blastShiftConcat
                            (blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                            { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                        {
                          lhs :=
                            ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯,
                          rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                    {
                      lhs :=
                        (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯).cast
                          ⋯,
                      rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).aig
                {
                  discr :=
                    (BVPred.mkUlt
                        (blastSub
                            (blastShiftConcat
                                (blastShiftConcat
                                    (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                    { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                            {
                              lhs :=
                                ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                  ⋯,
                              rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                        {
                          lhs :=
                            (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                  ⋯).cast
                              ⋯,
                          rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).ref,
                  lhs :=
                    (((blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                    { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).vec.cast
                              ⋯).cast
                          ⋯).cast
                      ⋯,
                  rhs :=
                    ((blastShiftConcat
                                (blastShiftConcat
                                    (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                    { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).vec.cast
                          ⋯).cast
                      ⋯ }).aig
            {
              discr :=
                (BVPred.mkUlt
                        (blastSub
                            (blastShiftConcat
                                (blastShiftConcat
                                    (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                    { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                            {
                              lhs :=
                                ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                  ⋯,
                              rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                        {
                          lhs :=
                            (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                  ⋯).cast
                              ⋯,
                          rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).ref.cast
                  ⋯,
              lhs :=
                (((((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯).cast
                          ⋯).cast
                      ⋯).cast
                  ⋯,
              rhs :=
                ((blastSub
                            (blastShiftConcat
                                (blastShiftConcat
                                    (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                    { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                            {
                              lhs :=
                                ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                  ⋯,
                              rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).vec.cast
                      ⋯).cast
                  ⋯ }).vec,
      hle := ⋯ } =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    {
            aig :=
              (AIG.RefVec.ite
                  (AIG.RefVec.ite
                      (BVPred.mkUlt
                          (blastSub
                              (blastShiftConcat
                                  (blastShiftConcat
                                      (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                      { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                  { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                              {
                                lhs :=
                                  ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                    ⋯,
                                rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                          {
                            lhs :=
                              (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                    ⋯).cast
                                ⋯,
                            rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).aig
                      {
                        discr :=
                          (BVPred.mkUlt
                              (blastSub
                                  (blastShiftConcat
                                      (blastShiftConcat
                                          (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                          { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                      { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                                  {
                                    lhs :=
                                      ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast
                                            ⋯).cast
                                        ⋯,
                                    rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                              {
                                lhs :=
                                  (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast
                                            ⋯).cast
                                        ⋯).cast
                                    ⋯,
                                rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).ref,
                        lhs :=
                          (((blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                          { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).vec.cast
                                    ⋯).cast
                                ⋯).cast
                            ⋯,
                        rhs :=
                          ((blastShiftConcat
                                      (blastShiftConcat
                                          (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                          { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                      { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).vec.cast
                                ⋯).cast
                            ⋯ }).aig
                  {
                    discr :=
                      (BVPred.mkUlt
                              (blastSub
                                  (blastShiftConcat
                                      (blastShiftConcat
                                          (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                          { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                      { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                                  {
                                    lhs :=
                                      ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast
                                            ⋯).cast
                                        ⋯,
                                    rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                              {
                                lhs :=
                                  (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast
                                            ⋯).cast
                                        ⋯).cast
                                    ⋯,
                                rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).ref.cast
                        ⋯,
                    lhs :=
                      (((((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯).cast
                                ⋯).cast
                            ⋯).cast
                        ⋯,
                    rhs :=
                      ((blastSub
                                  (blastShiftConcat
                                      (blastShiftConcat
                                          (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                          { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                      { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                                  {
                                    lhs :=
                                      ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast
                                            ⋯).cast
                                        ⋯,
                                    rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).vec.cast
                            ⋯).cast
                        ⋯ }).aig,
            wn := wn - 1, wr := wr + 1,
            q :=
              (AIG.RefVec.ite
                      (BVPred.mkUlt
                          (blastSub
                              (blastShiftConcat
                                  (blastShiftConcat
                                      (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                      { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                  { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                              {
                                lhs :=
                                  ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                    ⋯,
                                rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                          {
                            lhs :=
                              (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                    ⋯).cast
                                ⋯,
                            rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).aig
                      {
                        discr :=
                          (BVPred.mkUlt
                              (blastSub
                                  (blastShiftConcat
                                      (blastShiftConcat
                                          (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                          { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                      { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                                  {
                                    lhs :=
                                      ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast
                                            ⋯).cast
                                        ⋯,
                                    rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                              {
                                lhs :=
                                  (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast
                                            ⋯).cast
                                        ⋯).cast
                                    ⋯,
                                rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).ref,
                        lhs :=
                          (((blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                          { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).vec.cast
                                    ⋯).cast
                                ⋯).cast
                            ⋯,
                        rhs :=
                          ((blastShiftConcat
                                      (blastShiftConcat
                                          (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                          { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                      { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).vec.cast
                                ⋯).cast
                            ⋯ }).vec.cast
                ⋯,
            r :=
              (AIG.RefVec.ite
                  (AIG.RefVec.ite
                      (BVPred.mkUlt
                          (blastSub
                              (blastShiftConcat
                                  (blastShiftConcat
                                      (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                      { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                  { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                              {
                                lhs :=
                                  ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                    ⋯,
                                rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                          {
                            lhs :=
                              (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast
                                    ⋯).cast
                                ⋯,
                            rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).aig
                      {
                        discr :=
                          (BVPred.mkUlt
                              (blastSub
                                  (blastShiftConcat
                                      (blastShiftConcat
                                          (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                          { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                      { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                                  {
                                    lhs :=
                                      ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast
                                            ⋯).cast
                                        ⋯,
                                    rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                              {
                                lhs :=
                                  (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast
                                            ⋯).cast
                                        ⋯).cast
                                    ⋯,
                                rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).ref,
                        lhs :=
                          (((blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                          { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).vec.cast
                                    ⋯).cast
                                ⋯).cast
                            ⋯,
                        rhs :=
                          ((blastShiftConcat
                                      (blastShiftConcat
                                          (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                          { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                      { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).vec.cast
                                ⋯).cast
                            ⋯ }).aig
                  {
                    discr :=
                      (BVPred.mkUlt
                              (blastSub
                                  (blastShiftConcat
                                      (blastShiftConcat
                                          (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                          { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                      { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                                  {
                                    lhs :=
                                      ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast
                                            ⋯).cast
                                        ⋯,
                                    rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                              {
                                lhs :=
                                  (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast
                                            ⋯).cast
                                        ⋯).cast
                                    ⋯,
                                rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).ref.cast
                        ⋯,
                    lhs :=
                      (((((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯).cast
                                ⋯).cast
                            ⋯).cast
                        ⋯,
                    rhs :=
                      ((blastSub
                                  (blastShiftConcat
                                      (blastShiftConcat
                                          (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                          { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                                      { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                                  {
                                    lhs :=
                                      ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast
                                            ⋯).cast
                                        ⋯,
                                    rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).vec.cast
                            ⋯).cast
                        ⋯ }).vec,
            hle := ⋯ }.aig.decls.size
⊢ idx✝ <
    (blastSub
            (blastShiftConcat
                (blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                    { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
            { lhs := ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯,
              rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig.decls.size