proposition: Lemma ex6_res3 i: inc i L -> ex6_gij (J i i) = identity (ex6_Fl i).
proof: Proof. move => iL. have H: gle rL i i by apply:(proj32 HLp); rewrite HLs. apply: (identity_prop0 (ex6_res2 H)) => x xs. rewrite (ex6_gij_prop1 H). move: xs; rewrite (ex6_res1 H) => /inductive_limit_hi /= [ha]; rewrite !LgV// => hb ->. by rewrite (inl_restr_cf_ev (ex6_prop5c H) ha hb) (ex6_prop6b H). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)