proposition: Lemma prl_exa2_prop2: projective_limit prl_exa2_system = diagonal_graphp F I.
proof: Proof. have pa: domain (psE prl_exa2_system) = I by simpl; aw. set_extens t. move/prl_limitP => [qa qb qc hb]; apply /diagonal_graph_P. rewrite qb; split => //. split => // i j; rewrite qb /= => iI jI. move:(rdr iI jI) => [k [_ km2 kl2]]. rewrite (hb _ _ km2) (hb _ _ kl2). by rewrite (cst_graph_ev _ km2) (cst_graph_ev _ kl2). move => s /(range_gP qa) [u ud ->]; rewrite qb in ud. by move: (qc _ ud); rewrite LgV// - pa. move => /diagonal_graph_P [[ha hb] hc hd]; apply /prl_limitP; split => //. by move => i ide /=; rewrite LgV//; apply/ hd /(range_gP ha); exists i => //; rewrite hc. move => i j lea1. have idr: inc i (substrate r) by order_tac. have idt: inc i (domain t) by rewrite hc - sr. have jdr: inc j (substrate r) by order_tac. have jdt: inc j (domain t) by rewrite hc - sr. have hae:inc (Vg t j) F by apply/ hd /(range_gP ha); exists j. rewrite !LgV// idV//; exact:(hb _ _ idt jdt). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)