proposition: Lemma inl_map2_compat_prop1 S S' u x i j: inl_same_index S S' -> inl_map2_compat S S' u -> inc x (Vg (isE S) i) -> gle (isr S) i j -> class (inl_equiv S') (J (Vf (Vg u i) x) i) = class (inl_equiv S') (J (Vf (Vg u j) (Vf (Vg (isf S) (J i j)) x)) j).
proof: Proof. move => ha hb xE lij. rewrite - (inl_map2_compat_prop0 ha hb xE lij). move: (proj43 hb _(proj1 (inl_prop0 lij))) =>[fui sui tui]. rewrite ha in lij; rewrite(inl_class_of_fij lij)//; Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)