proposition: Lemma prl_dl3_systemS_can: bijection_prop iso (projective_limit prl_dl3_systemS) (productb E).
proof: Proof. rewrite - prl_dl3_RHS. exact: (prl_dl_canon_bijection or prl_dl3_orL sr prl_dl3_srL prl_dl3_systemS_sr). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)