Definition lcoset_in_rcoset_property {X : gr} {N : subgr X} (H : lcoset_in_rcoset N) (g : X) (n1 : N) : N (pr1 (lcoset_in_rcoset_witness H g n1)) := pr2 (lcoset_in_rcoset_witness H g n1).
Require Import UniMath.MoreFoundations.Subtypes.