Add a generic UARel lemma to prove EquivJ for groups

[ecavallo]

Any univalent reflexive graph has a version of EquivJ, so we don't have to prove this by hand. I didn't look to see if this is also proven by hand for algebraic structures other than groups, but if you point me to some I can update those too.

[felixwellen]

Very nice! I don't remember seeing any other instances... so I'll just merge this.