proposition: Lemma Lgd x p: domain (Lg x p) = x.
proof: Proof. set_extens t. by case/funI_P => [e /funI_P [z zx ->] ->]; aw. by move => tw;apply/funI_P; exists (J t (p t)); aw => //;apply:Lg_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)