{P : Sort u_1} →
  {i : Type u} →
    {t : Lean.Doc.MarkdownInline i} →
      {i' : Type u} →
        {t' : Lean.Doc.MarkdownInline i'} → i = i' → t ≍ t' → Lean.Doc.MarkdownInline.noConfusionType P t t'