(motive : Std.Format → Bool → ℤ → ℕ → Sort u_1) →
  (x : Std.Format) →
    (x_1 : Bool) →
      (x_2 : ℤ) →
        (x_3 : ℕ) →
          ((x : Bool) → (x_4 : ℤ) → (x_5 : ℕ) → motive Std.Format.nil x x_4 x_5) →
            ((flatten : Bool) → (x : ℤ) → (x_4 : ℕ) → motive Std.Format.line flatten x x_4) →
              ((force flatten : Bool) → (m : ℤ) → (w : ℕ) → motive (Std.Format.align force) flatten m w) →
                ((s : String) → (flatten : Bool) → (x : ℤ) → (x_4 : ℕ) → motive (Std.Format.text s) flatten x x_4) →
                  ((f₁ f₂ : Std.Format) → (flatten : Bool) → (m : ℤ) → (w : ℕ) → motive (f₁.append f₂) flatten m w) →
                    ((n : ℤ) →
                        (f : Std.Format) →
                          (flatten : Bool) → (m : ℤ) → (w : ℕ) → motive (Std.Format.nest n f) flatten m w) →
                      ((f : Std.Format) →
                          (behavior : Std.Format.FlattenBehavior) →
                            (x : Bool) → (m : ℤ) → (w : ℕ) → motive (f.group behavior) x m w) →
                        ((a : ℕ) →
                            (f : Std.Format) →
                              (flatten : Bool) → (m : ℤ) → (w : ℕ) → motive (Std.Format.tag a f) flatten m w) →
                          motive x x_1 x_2 x_3