proposition: Lemma prl_exa1_prop2: projective_limit prl_exa1_system = 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 /=. have hu: inc (J i i) (diagonal I) by rewrite {2} ea. by move/setXb_P: tp => [_ _ px]; rewrite LgV// idV//;aw; apply: px; rewrite dE. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)