{P : Sort u} →
  {name type : String} →
    {doc? : Option String} →
      {name' type' : String} →
        {doc?' : Option String} →
          { name := name, type := type, doc? := doc? } = { name := name', type := type', doc? := doc?' } →
            (name = name' → type = type' → doc? = doc?' → P) → P