cut (G \sub (ι(G \sub O · G \sub x)) = G \sub (ι(G \sub O · G \sub y)));
[ rewrite > (repr_index_of ? ? (G \sub O · G \sub x)) in Hcut;
rewrite > (repr_index_of ? ? (G \sub O · G \sub y)) in Hcut;
cut (G \sub (ι(G \sub O · G \sub x)) = G \sub (ι(G \sub O · G \sub y)));
[ rewrite > (repr_index_of ? ? (G \sub O · G \sub x)) in Hcut;
rewrite > (repr_index_of ? ? (G \sub O · G \sub y)) in Hcut;