∀ (x x_1 x_2 x_3 : WellOrder),
  x ≈ x_2 →
    x_1 ≈ x_3 →
      (match x with
        | { α := α, r := r, wo := wo } =>
          match x_1 with
          | { α := α_1, r := s, wo := wo } => Nonempty (InitialSeg r s)) =
        match x_2 with
        | { α := α, r := r, wo := wo } =>
          match x_3 with
          | { α := α_1, r := s, wo := wo } => Nonempty (InitialSeg r s)