(motive : String → Sort u_1) →
  (tag : String) →
    (Unit → motive "target") →
      (Unit → motive "hyp") →
        (Unit → motive "hypType") → (Unit → motive "hypValue") → ((x : String) → motive x) → motive tag