{w : ℕ} →
  (lw : ℕ) →
    (llhs : Std.Tactic.BVDecide.BVExpr w) →
      (lrhs : Std.Tactic.BVDecide.BVExpr lw) →
        (motive : (r : Std.Tactic.BVDecide.BVExpr w) → ¬hash (llhs.shiftLeft lrhs) ≠ hash r → Sort u_1) →
          (r : Std.Tactic.BVDecide.BVExpr w) →
            (h : ¬hash (llhs.shiftLeft lrhs) ≠ hash r) →
              ((rw : ℕ) →
                  (rlhs : Std.Tactic.BVDecide.BVExpr w) →
                    (rrhs : Std.Tactic.BVDecide.BVExpr rw) →
                      (h : ¬hash (llhs.shiftLeft lrhs) ≠ hash (rlhs.shiftLeft rrhs)) → motive (rlhs.shiftLeft rrhs) h) →
                ((val : BitVec w) →
                    (h : ¬hash (llhs.shiftLeft lrhs) ≠ hash (Std.Tactic.BVDecide.BVExpr.const val)) →
                      motive (Std.Tactic.BVDecide.BVExpr.const val) h) →
                  ((idx : ℕ) →
                      (h : ¬hash (llhs.shiftLeft lrhs) ≠ hash (Std.Tactic.BVDecide.BVExpr.var idx)) →
                        motive (Std.Tactic.BVDecide.BVExpr.var idx) h) →
                    ((w_1 start : ℕ) →
                        (expr : Std.Tactic.BVDecide.BVExpr w_1) →
                          (h : ¬hash (llhs.shiftLeft lrhs) ≠ hash (Std.Tactic.BVDecide.BVExpr.extract start w expr)) →
                            motive (Std.Tactic.BVDecide.BVExpr.extract start w expr) h) →
                      ((lhs : Std.Tactic.BVDecide.BVExpr w) →
                          (op : Std.Tactic.BVDecide.BVBinOp) →
                            (rhs : Std.Tactic.BVDecide.BVExpr w) →
                              (h : ¬hash (llhs.shiftLeft lrhs) ≠ hash (lhs.bin op rhs)) → motive (lhs.bin op rhs) h) →
                        ((op : Std.Tactic.BVDecide.BVUnOp) →
                            (operand : Std.Tactic.BVDecide.BVExpr w) →
                              (h : ¬hash (llhs.shiftLeft lrhs) ≠ hash (Std.Tactic.BVDecide.BVExpr.un op operand)) →
                                motive (Std.Tactic.BVDecide.BVExpr.un op operand) h) →
                          ((l r : ℕ) →
                              (lhs : Std.Tactic.BVDecide.BVExpr l) →
                                (rhs : Std.Tactic.BVDecide.BVExpr r) →
                                  (h : w = l + r) →
                                    (h_7 : ¬hash (llhs.shiftLeft lrhs) ≠ hash (lhs.append rhs h)) →
                                      motive (lhs.append rhs h) h_7) →
                            ((w_1 n : ℕ) →
                                (expr : Std.Tactic.BVDecide.BVExpr w_1) →
                                  (h : w = w_1 * n) →
                                    (h_8 :
                                        ¬hash (llhs.shiftLeft lrhs) ≠
                                            hash (Std.Tactic.BVDecide.BVExpr.replicate n expr h)) →
                                      motive (Std.Tactic.BVDecide.BVExpr.replicate n expr h) h_8) →
                              ((n : ℕ) →
                                  (lhs : Std.Tactic.BVDecide.BVExpr w) →
                                    (rhs : Std.Tactic.BVDecide.BVExpr n) →
                                      (h : ¬hash (llhs.shiftLeft lrhs) ≠ hash (lhs.shiftRight rhs)) →
                                        motive (lhs.shiftRight rhs) h) →
                                ((n : ℕ) →
                                    (lhs : Std.Tactic.BVDecide.BVExpr w) →
                                      (rhs : Std.Tactic.BVDecide.BVExpr n) →
                                        (h : ¬hash (llhs.shiftLeft lrhs) ≠ hash (lhs.arithShiftRight rhs)) →
                                          motive (lhs.arithShiftRight rhs) h) →
                                  motive r h