proposition: Lemma noid_inl_class_compat i j x y (R := (inl_equiv noid_ind_system) ): inc i I -> inc j I -> inc x (Vg noid_E' i) -> inc y (Vg noid_E' j) -> (class R (J x i) = class R (J y j) <-> class noid_inl_equiv (J x i) = class noid_inl_equiv (J y j)).
proof: Proof. move => iI jI xE yE. move:(@inl_class_eq_bis noid_ind_system i j x y) => /= h. apply: (iff_trans (h iI jI xE yE)); clear h. have xixU: inc (J x i) noid_inl_sum. by apply/noid_inl_sumP;split; aw; fprops; apply: noid_prop5a. have yjxU: inc (J y j) noid_inl_sum. by apply/noid_inl_sumP;split; aw; fprops; apply: noid_prop5a. move:noid_inl_equiv_esr => [Er Sr]. split. move=> [k /= []]; aw; move => leik lejk. rewrite (noid_prop5c leik xE) (noid_prop5c lejk yE) => vv. apply:(class_eq1 Er); apply/graph_on_P1; split => //. - by exists k; aw. rewrite - Sr in xixU yjxU => xx. move/ (related_equiv_P Er): (And3 xixU yjxU xx) => /graph_on_P1 [_ _]. move =>[k []]; aw =>leik lejk etc; exists k; simpl; saw. by rewrite (noid_prop5c leik xE) (noid_prop5c lejk yE). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)