(motive : Std.Format → Sort u_1) →
  (x : Std.Format) →
    (Unit → motive Std.Format.nil) →
      (Unit → motive Std.Format.line) →
        ((force : Bool) → motive (Std.Format.align force)) →
          ((msg : String) → motive (Std.Format.text msg)) →
            ((indent : ℤ) → (f : Std.Format) → motive (Std.Format.nest indent f)) →
              ((f₁ f₂ : Std.Format) → motive (f₁.append f₂)) →
                ((f : Std.Format) → (behavior : Std.Format.FlattenBehavior) → motive (f.group behavior)) →
                  ((a : ℕ) → (f : Std.Format) → motive (Std.Format.tag a f)) → motive x