∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (c : OmegaCompletePartialOrder.Chain α) {f : α →o β} (g : β →o γ), (c.map f).map g = c.map (g.comp f)