proposition: Lemma inl_class_eq_bis S i j x y: inc i (isI S) -> inc j (isI S) -> inc x (Vg (isE S) i) -> inc y (Vg (isE S) j) -> (class (inl_equiv S) (J x i) = class (inl_equiv S) (J y j) <-> inl_equiv_rel S (J x i) (J y j)).
proof: Proof. move => ha hb hc hd. by apply: inl_class_eq; apply/inl_sumP; aw; split; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)