proposition: Lemma ex1_prop6 i j (lij: gle rL i j) : prl_same_data (prl_restr (ex1_prop5 lij)) (ex1_systemi i).
proof: Proof. have r1 := HJm lij. have [iL jL]:= (ex1_prop2 lij). have Hu:= (ex1_prop4 jL). apply:prl_same_dataT (ex1_prop5b (sub_trans r1 Hu) iL). apply:prl_same_dataT (projective_limit_restr_double_Iv Hu r1). apply:prl_restr_Iv2. exact: (prl_same_dataS (ex1_prop5b Hu jL)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)