proposition: Lemma related_rep_class x: inc x (substrate r) -> related r x (rep (class r x)).
proof: Proof. move=> xs. suff: related r (rep (class r x)) x by move=> h; equiv_tac. by apply: related_rep_in_class; fprops; apply: inc_itself_class. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)