(motive :
    (u : Lean.Level) →
      {α : Q(Type u)} →
        (x : Q(Zero «$α»)) →
          (x_1 : Q(PartialOrder «$α»)) →
            (e : Q(«$α»)) →
              Lean.MetaM (Mathlib.Meta.Positivity.Strictness x x_1 e) →
                Lean.MetaM (Mathlib.Meta.Positivity.Strictness x x_1 e) → Sort u_1) →
  (u : Lean.Level) →
    {α : Q(Type u)} →
      (x : Q(Zero «$α»)) →
        (x_1 : Q(PartialOrder «$α»)) →
          (e : Q(«$α»)) →
            (__alt __alt_1 : Lean.MetaM (Mathlib.Meta.Positivity.Strictness x x_1 e)) →
              ((α : Q(Type)) →
                  (x : Q(Zero «$α»)) →
                    (x_2 : Q(PartialOrder «$α»)) →
                      (e : Q(«$α»)) →
                        (__alt __alt_2 : Lean.MetaM (Mathlib.Meta.Positivity.Strictness x x_2 e)) →
                          motive Lean.Level.zero x x_2 e __alt __alt_2) →
                ((x : Lean.Level) →
                    (α : Q(Type x)) →
                      (x_2 : Q(Zero «$α»)) →
                        (x_3 : Q(PartialOrder «$α»)) →
                          (e : Q(«$α»)) →
                            (__alt __alt_2 : Lean.MetaM (Mathlib.Meta.Positivity.Strictness x_2 x_3 e)) →
                              motive x x_2 x_3 e __alt __alt_2) →
                  motive u x x_1 e __alt __alt_1