{u : Lean.Level} →
  {α : Q(Type u)} →
    {a b : Q(«$α»)} →
      (motive : Mathlib.Meta.NormNum.Result a → Mathlib.Meta.NormNum.Result b → Sort u_1) →
        (ra : Mathlib.Meta.NormNum.Result a) →
          (rb : Mathlib.Meta.NormNum.Result b) →
            ((val : Bool) →
                (proof : Lean.Expr) →
                  (x : Mathlib.Meta.NormNum.Result b) → motive (Mathlib.Meta.NormNum.Result'.isBool val proof) x) →
              ((x : Mathlib.Meta.NormNum.Result a) →
                  (val : Bool) → (proof : Lean.Expr) → motive x (Mathlib.Meta.NormNum.Result'.isBool val proof)) →
                ((inst : Q(DivisionSemiring «$α»)) →
                    (q : ℚ) →
                      (n d : Q(ℕ)) →
                        (proof : Q(Mathlib.Meta.NormNum.IsNNRat «$a» «$n» «$d»)) →
                          (x : Mathlib.Meta.NormNum.Result b) →
                            motive (Mathlib.Meta.NormNum.Result'.isNNRat inst q n d proof) x) →
                  ((x : Mathlib.Meta.NormNum.Result a) →
                      (inst : Q(DivisionSemiring «$α»)) →
                        (q : ℚ) →
                          (n d : Q(ℕ)) →
                            (proof : Q(Mathlib.Meta.NormNum.IsNNRat «$b» «$n» «$d»)) →
                              motive x (Mathlib.Meta.NormNum.Result'.isNNRat inst q n d proof)) →
                    ((inst : Q(DivisionRing «$α»)) →
                        (q : ℚ) →
                          (n d : Q(ℕ)) →
                            (proof : Q(Mathlib.Meta.NormNum.IsRat «$a» (Int.negOfNat «$n») «$d»)) →
                              (x : Mathlib.Meta.NormNum.Result b) →
                                motive (Mathlib.Meta.NormNum.Result'.isNegNNRat inst q n d proof) x) →
                      ((x : Mathlib.Meta.NormNum.Result a) →
                          (inst : Q(DivisionRing «$α»)) →
                            (q : ℚ) →
                              (n d : Q(ℕ)) →
                                (proof : Q(Mathlib.Meta.NormNum.IsRat «$b» (Int.negOfNat «$n») «$d»)) →
                                  motive x (Mathlib.Meta.NormNum.Result'.isNegNNRat inst q n d proof)) →
                        ((inst : Q(Ring «$α»)) →
                            (lit : Q(ℕ)) →
                              (proof : Q(Mathlib.Meta.NormNum.IsInt «$a» (Int.negOfNat «$lit»))) →
                                (x : Mathlib.Meta.NormNum.Result b) →
                                  motive (Mathlib.Meta.NormNum.Result'.isNegNat inst lit proof) x) →
                          ((x : Mathlib.Meta.NormNum.Result a) →
                              (inst : Q(Ring «$α»)) →
                                (lit : Q(ℕ)) →
                                  (proof : Q(Mathlib.Meta.NormNum.IsInt «$b» (Int.negOfNat «$lit»))) →
                                    motive x (Mathlib.Meta.NormNum.Result'.isNegNat inst lit proof)) →
                            ((ra : Q(AddMonoidWithOne «$α»)) →
                                (na : Q(ℕ)) →
                                  (pa : Q(Mathlib.Meta.NormNum.IsNat «$a» «$na»)) →
                                    (rb : Q(AddMonoidWithOne «$α»)) →
                                      (nb : Q(ℕ)) →
                                        (pb : Q(Mathlib.Meta.NormNum.IsNat «$b» «$nb»)) →
                                          motive (Mathlib.Meta.NormNum.Result'.isNat ra na pa)
                                            (Mathlib.Meta.NormNum.Result'.isNat rb nb pb)) →
                              motive ra rb