∀ {α : Type u_1} (motive : Ordnode α → Prop) (x : Ordnode α),
  (∀ (a : Unit), motive Ordnode.nil) →
    (∀ (size : ℕ) (l : Ordnode α) (y : α) (r : Ordnode α), motive (Ordnode.node size l y r)) → motive x