∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop}
  [inst : IsWellOrder β s] [inst_1 : IsTrans γ t] (f : InitialSeg r s) (g : PrincipalSeg s t) (a : α),
  (f.transPrincipal g).toRelEmbedding a = g.toRelEmbedding (f a)