proposition: Lemma reflexive_domain g: reflexivep g -> domain g = substrate g.
proof: Proof. move=> pb; set_extens u; first by apply: setU2_1. case /setU2_P => // ug; apply/funI_P; exists (J u u);aw; trivial. exact:(pb _ (setU2_2 (domain g) ug)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)