apply (H ? ? ? GaxGax)
| unfold is_right_unit; intro;
letin GaxGax ≝ (refl_eq ? (x·G \sub a));
clearbody GaxGax;
rewrite < GaGa in GaxGax:(? ? % ?);
apply (H ? ? ? GaxGax)
| unfold is_right_unit; intro;
letin GaxGax ≝ (refl_eq ? (x·G \sub a));
clearbody GaxGax;
rewrite < GaGa in GaxGax:(? ? % ?);