proposition: Lemma prl_dl3_RHS: (projective_limit S') = productb E.
proof: Proof. set_extens t; [ by case/Zo_P | move => tp; apply:(Zo_i tp)]. move => i j ilj; move/diagonal_pi_P:(ilj) => [iI ea]; rewrite - ea /=. rewrite - [Lg _ _]/(psf S') ps_identity_f // idV //. by move/setXb_P: tp => [_ _ px]; apply: px => //; rewrite /E; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)