lemma gr_eq_inv_next_uni (n) (g): āg ā” š®āØnā© ā ā§ā§ š®āØānā© ā” g & āān = n.
/3 width=1 by gr_eq_inv_uni_next, gr_eq_sym/ qed-.
lemma gr_eq_inv_next_uni (n) (g): āg ā” š®āØnā© ā ā§ā§ š®āØānā© ā” g & āān = n.
/3 width=1 by gr_eq_inv_uni_next, gr_eq_sym/ qed-.