proposition: Lemma inl_map_injective S u F: inl_map_compat S u F -> (injection (inductive_map S u F) <-> forall i x y, inc i (isI S) -> inc x (Vg (isE S) i) -> inc y (Vg (isE S) i) -> Vf (Vg u i) x = Vf (Vg u i) y -> exists2 j, gle (isr S) i j & Vf (Vg (isf S) (J i j)) x = Vf (Vg (isf S) (J i j)) y).
proof: Proof. move => h0. move:(inl_map_prop h0) => h1. move: (h1) => [[fu su tu] cu]. have [eqv seqv]:=(inl_equiv_esr S). split. move=> [_ inj] i x y iI xE yE sv. rewrite su in inj. move: (inl_class_in_lim iI xE) (inl_class_in_lim iI yE) => c1 c2. move: sv; rewrite -(inl_inductive_map_ev h0 iI xE). rewrite -(inl_inductive_map_ev h0 iI yE) => ee. move: (inj _ _ c1 c2 ee). by move => /(inl_class_eq_bis iI iI xE yE) [k []]; aw => ha _ hb; exists k. move => h. split => //; rewrite su => x y /inductive_limit_hi [rxi rxE ->]. move /inductive_limit_hi => [ryi ryE ->]. rewrite (inl_map_property_res1 h0 h1 rxi rxE). rewrite (inl_map_property_res1 h0 h1 ryi ryE). move:(is_directed_r rxi ryi) => [k [kI lik ljk]]. rewrite (inl_map_compat0 h0 lik rxE) (inl_map_compat0 h0 ljk ryE). set xa := (Vf (Vg (isf S) (J (Q (rep x)) k)) _). set ya := (Vf (Vg (isf S) (J (Q (rep y)) k)) _) => eqa. move: (inl_prop4 lik) => [fik sik tik]. move: (inl_prop4 ljk) => [fjk sjk tjk]. have xas: inc xa (Vg (isE S) k) by rewrite /xa; Wtac. have yas: inc ya (Vg (isE S) k) by rewrite /ya; Wtac. rewrite -(inl_class_of_fij lik rxE) - (inl_class_of_fij ljk ryE). apply/(inl_class_eq_bis kI kI xas yas). move:(h _ _ _ kI xas yas eqa) => [j lkj jp]. exists j; saw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)