proposition: Lemma inl_class_of_fij S i j x: gle (isr S) i j -> inc x (Vg (isE S) i) -> class (inl_equiv S) (J (Vf (Vg (isf S) (J i j)) x) j) = class (inl_equiv S) (J x i).
proof: Proof. move => lij xE. move: (inl_prop0 lij) => [iI jI]. move: (inl_prop4 lij) => [fij sij tij]. have fiE:inc (Vf (Vg (isf S) (J i j)) x) (Vg (isE S) j) by Wtac. symmetry;apply/(inl_class_eq_bis iI jI xE fiE). exists j; aw; split => //; first exact:inl_prop1. rewrite (inl_prop5 jI) //; Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)