{u : Lean.Level} →
  {α : Q(Type u)} →
    {s : Q(List «$α»)} →
      {motive : Mathlib.Meta.List.ProveNilOrConsResult s → Sort u} →
        (t : Mathlib.Meta.List.ProveNilOrConsResult s) →
          t.ctorIdx = 1 →
            ((a : Q(«$α»)) →
                (s' : Q(List «$α»)) →
                  (pf : Q(«$s» = «$a» :: «$s'»)) → motive (Mathlib.Meta.List.ProveNilOrConsResult.cons a s' pf)) →
              motive t