∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DecidableLE α] (x : α) {t : Ordnode α} {a₁ : WithBot α} {a₂ : WithTop α},
  Ordnode.Valid' a₁ t a₂ → Ordnode.Valid' a₁ (Ordnode.erase x t) a₂ ∧ Ordnode.Raised (Ordnode.erase x t).size t.size