proposition: Lemma inl_class_eq S x y: inc x (inl_sum S) -> inc y (inl_sum S) -> (class (inl_equiv S) x = class (inl_equiv S) y <-> inl_equiv_rel S x y).
proof: Proof. have [ha hb] := inl_equiv_esr S. move => xE yE; move: (xE)(yE); rewrite - hb => xsr ysr. split => xx. by move/(related_equiv_P ha): (And3 xsr ysr xx) => /graph_on_P1 []. by apply/(class_eq1 ha); apply/graph_on_P1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)