∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : Mul A] [inst_1 : Mul B] [inst_2 : Mul C] [inst_3 : Star A]
  [inst_4 : Star B] [inst_5 : Star C] (e₁ : A ≃⋆* B) (e₂ : B ≃⋆* C), (e₁.trans e₂).toMulEquiv = e₁.trans e₂.toMulEquiv