(motive :
    (u : Lean.Level) →
      {αZ : Q(Type u)} →
        (e : Q(«$αZ»)) →
          Lean.MetaM (Mathlib.Meta.NormNum.Result e) → Lean.MetaM (Mathlib.Meta.NormNum.Result e) → Sort u_1) →
  (u : Lean.Level) →
    {αZ : Q(Type u)} →
      (e : Q(«$αZ»)) →
        (__alt __alt_1 : Lean.MetaM (Mathlib.Meta.NormNum.Result e)) →
          ((αZ : Q(Type)) →
              (e : Q(«$αZ»)) →
                (__alt __alt_2 : Lean.MetaM (Mathlib.Meta.NormNum.Result e)) → motive Lean.Level.zero e __alt __alt_2) →
            ((x : Lean.Level) →
                (αZ : Q(Type x)) →
                  (e : Q(«$αZ»)) →
                    (__alt __alt_2 : Lean.MetaM (Mathlib.Meta.NormNum.Result e)) → motive x e __alt __alt_2) →
              motive u e __alt __alt_1