let funType_1 := fun x x_1 x_2 => String.utf8Len x ≤ String.utf8Len x_1;
∀ (motive : (x x_1 : List Char) → (x_2 : x.Sublist x_1) → List.Sublist.below x_2 → Prop) (x x_1 : List Char)
  (x_2 : x.Sublist x_1) (below : List.Sublist.below x_2),
  (∀ (a : Unit), motive [] [] ⋯ ⋯) →
    (∀ (x l₂ : List Char) (a : Char) (h : x.Sublist l₂) (ih : List.Sublist.below h) (a_ih : funType_1 x l₂ h),
        motive x (a :: l₂) ⋯ ⋯) →
      (∀ (l₁ l₂ : List Char) (a : Char) (h : l₁.Sublist l₂) (ih : List.Sublist.below h) (a_ih : funType_1 l₁ l₂ h),
          motive (a :: l₁) (a :: l₂) ⋯ ⋯) →
        motive x x_1 x_2 below