proposition: Lemma prl_trivial S: psI S = emptyset -> projective_limit S = singleton emptyset.
proof: Proof. move => h. set_extens t. move => /prl_limitP[fgt dt _ _ ]. rewrite - (Lg_recovers fgt) dt h /Lg funI_set0; fprops. move/set1_P => ->; apply /prl_limitP; split => //. - apply: fgraph_set0. - by rewrite domain_set0. - by rewrite h => i /in_set0. - by move => i j /prl_prop0 []; rewrite h => /in_set0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)