(motive : String → Sort u_1) →
  (tag : String) →
    (Unit → motive "goal") →
      (Unit → motive "expr") →
        (Unit → motive "widget") → (Unit → motive "trace") → ((x : String) → motive x) → motive tag