{motive : Mathlib.Meta.FunProp.Theorem → Sort u} →
  (t : Mathlib.Meta.FunProp.Theorem) →
    ((thm : Mathlib.Meta.FunProp.LambdaTheorem) → motive (Mathlib.Meta.FunProp.Theorem.lam thm)) →
      ((thm : Mathlib.Meta.FunProp.FunctionTheorem) → motive (Mathlib.Meta.FunProp.Theorem.function thm)) →
        ((thm : Mathlib.Meta.FunProp.GeneralTheorem) → motive (Mathlib.Meta.FunProp.Theorem.mor thm)) →
          ((thm : Mathlib.Meta.FunProp.GeneralTheorem) → motive (Mathlib.Meta.FunProp.Theorem.transition thm)) →
            motive t