proposition: Lemma prl_dl3_mod_inj x y: inc x (projective_limit prl_dl3_systemS) -> inc y (projective_limit prl_dl3_systemS) -> (prl_dl3_mod x) = (prl_dl3_mod y) -> x = y.
proof: Proof. move => /prl_limitP /= [p1 p2 p3 _] /prl_limitP /= [q1 q2 q3 _]. rewrite /prl_dl3_mod => eq1. apply: fgraph_exten => //; rewrite p2 // => t /setX_P [pa pb pc]. by move: (f_equal (fun z => (Vg (Vg z (P t)) (Q t))) eq1); rewrite !LgV// pa. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)