∀ {α : Type u_1} (xs : List α) (motive : Ordnode α × { l' // l'.length ≤ xs.length } → Sort u_2) (l : Ordnode α) (y : α)
  (ys : List α) (h : (y :: ys).length ≤ xs.length)
  (h_1 : (t : Ordnode α) → (property : [].length ≤ xs.length) → motive (t, ⟨[], property⟩))
  (h_2 : (l : Ordnode α) → (y : α) → (ys : List α) → (h : (y :: ys).length ≤ xs.length) → motive (l, ⟨y :: ys, h⟩)),
  (match (l, ⟨y :: ys, h⟩) with
    | (t, ⟨[], property⟩) => h_1 t property
    | (l, ⟨y :: ys, h⟩) => h_2 l y ys h) =
    h_2 l y ys h