{motive : Lean.NamingContext → Sort u} →
  (t : Lean.NamingContext) →
    ((currNamespace : Lean.Name) →
        (openDecls : List Lean.OpenDecl) → motive { currNamespace := currNamespace, openDecls := openDecls }) →
      motive t