∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} (e : L ≃ᴸ L') (e' : L' ≃ᴸ L''),
  (e'.toLHom.comp e.toLHom).comp (e.invLHom.comp e'.invLHom) = FirstOrder.Language.LHom.id L''