proposition: Lemma inl_sub_fam_im3_val: forall i, inc i (isI S) -> class (inl_equiv S') (J (Vg a_fam i) i) = class (inl_equiv S') (J (Vg a_fam (rep (isI S))) (rep (isI S))).
proof: Proof. move: a_fam_prop=> [ha hb hc hd]. have II:= (inl_same_index_same_I sii). pose ci i := class (inl_equiv S') (J (Vg a_fam i) i). have h: forall i j, gle (isr S') i j -> ci i = ci j. move => i j lij. move: (inl_class_of_fij lij (hc _ (proj1 (inl_prop0 lij)))). by move:(hd _ lij); aw; move => ->. rewrite II => i iI. have rI: inc (rep (isI S')) (isI S') by apply:rep_i; ex_tac. move:(is_directed_r iI rI) => [k [kI ka kb]]. by rewrite -/(ci i ) (h _ _ ka) -(h _ _ kb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)