∀ {α : Type u_1} [inst : Preorder α] {β : Type u_2} [inst_1 : Preorder β] {f : α → β},
  StrictMono f →
    ∀ {t : Ordnode α} {a₁ : WithBot α} {a₂ : WithTop α},
      Ordnode.Valid' a₁ t a₂ →
        Ordnode.Valid' (Option.map f a₁) (Ordnode.map f t) (Option.map f a₂) ∧ (Ordnode.map f t).size = t.size