∀ {α : Type u_1} (x : List α),
  Ordnode.ofAscListAux₂ x =
    match (motive := List α → Ordnode α → ℕ → Ordnode α) x with
    | [] => fun t x => t
    | x :: xs => fun l s =>
      match Ordnode.ofAscListAux₁ xs s with
      | (r, ⟨ys, h⟩) =>
        have this := ⋯;
        Ordnode.ofAscListAux₂ ys (l.link x r) (s <<< 1)