proposition: Lemma rel_on_quoP2 p r: equivalence r -> compatible_with_equiv_p p r -> forall y, ( (inc y (substrate r) /\ relation_on_quotient p r (Vf (canon_proj r) y)) <-> (inc y (substrate r) /\ p y)).
proof: Proof. move=> er co; split; move => [ysr]; rewrite (canon_proj_V ysr). move => [tq [x xt px]]. have yx: related r x y by move : xt; move /(class_P er) => h; equiv_tac. by split =>//; apply: (co _ _ px yx). move => py;split =>//; split; fprops. move:(inc_itself_class er ysr) => h; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)