{m : Type → Type} →
  {motive : Std.Format.MonadPrettyFormat m → Sort u} →
    ((pushOutput : String → m Unit) →
        (pushNewline : ℕ → m Unit) →
          (currColumn : m ℕ) →
            (startTag endTags : ℕ → m Unit) →
              motive
                { pushOutput := pushOutput, pushNewline := pushNewline, currColumn := currColumn, startTag := startTag,
                  endTags := endTags }) →
      (t : Std.Format.MonadPrettyFormat m) → motive t