proposition: Lemma prl_limitP S x: inc x (projective_limit S) <-> [/\ fgraph x, domain x = psI S, forall i, inc i (psI S) -> inc (Vg x i) (Vg (psE S) i)& forall i j, gle (psr S) i j -> Vg x i = Vf (Vg (psf S) (J i j)) (Vg x j)].
proof: Proof. rewrite - ps_domain_E; split. by move => /Zo_P [/setXb_P [pa pb pc] pd]. by move => [pa pb pc pd]; apply/Zo_P; split => //; apply/setXb_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)