Lemma grtogtunel (X : gr) {R : hrel X} (is : isbinophrel R) {x : X} (isg : R 1 (x^-1)) : R x 1. Proof. assert (r := (pr2 is) _ _ x isg). rewrite (grlinvax X x) in r. rewrite (lunax X _) in r. apply r. Defined.
Require Import UniMath.MoreFoundations.Subtypes.