clearbody GOGO;
rewrite < HH in GOGO;
rewrite < HH in GOGO:(? ? % ?);
- rewrite > (associative ? G) in GOGO;
+ rewrite > (op_associative ? G) in GOGO;
letin GaGa ≝ (H ? ? ? GOGO);
clearbody GaGa;
clear GOGO;
letin GaxGax ≝ (refl_eq ? (G \sub a ·x));
clearbody GaxGax;
rewrite < GaGa in GaxGax:(? ? % ?);
- rewrite > (associative ? (semigroup_properties G)) in GaxGax;
+ rewrite > (op_associative ? (semigroup_properties G)) in GaxGax;
apply (H ? ? ? GaxGax)
| unfold is_right_unit; intro;
letin GaxGax ≝ (refl_eq ? (x·G \sub a));
clearbody GaxGax;
rewrite < GaGa in GaxGax:(? ? % ?);
- rewrite < (associative ? (semigroup_properties G)) in GaxGax;
+ rewrite < (op_associative ? (semigroup_properties G)) in GaxGax;
apply (H1 ? ? ? GaxGax)
]
]