-record isSemiGroup (M:Magma) : Prop ≝
- { op_associative: associative ? (op M) }.
-
-record SemiGroup : Type ≝
- { magma:> Magma;
- semigroup_properties:> isSemiGroup magma
+record SemiGroup : Type≝
+ { pre_semi_group:> PreSemiGroup;
+ is_semi_group :> IsSemiGroup pre_semi_group