proposition: Lemma prl_restr_trivial p: Lf (restr^~ (psI p)) (projective_limit p) (projective_limit p) = identity (projective_limit p).
proof: Proof. set E := projective_limit p. have pa x: inc x E -> (restr x (psI p)) = x. move => xE; move/prl_limitP:(xE) => [fgx dx xv xw]. by apply:fgraph_exten; fprops; aw; [ rewrite dx | aw => t tI; rewrite LgV//]. have pb: lf_axiom (restr^~ (psI p)) E E. by move => x xE; rewrite /= pa. apply:function_exten;aww; first by apply:lf_function. by move => x xE /=; rewrite LfV // idV // pa. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)