Lemma about simulations and initial segments of ordinals

[tomdjong]

@fredrikNordvallForsberg and I showed that

Given simulations
  f : α ⊴ γ and g : β ⊴ γ
and points a : α and b : β we have
  f a ≼ g b   ⇔   α ↓ a ⊴ β ↓ b,
and
  f a ＝ g b   ⇔   α ↓ a ≃ₒ β ↓ b.

This is preliminary work for a future PR on ordinal exponentation. In the process, we generalized some universe levels in existing constructions, i.e. we allowed the carriers of ordinals α and β to be in different universes.