proposition: Lemma substrate_prod_of_rel r r': equivalence r ->equivalence r' -> substrate (prod_of_relation r r') = (substrate r)\times (substrate r').
proof: Proof. move => pa pb; rewrite graph_on_sr //. by move => a /setX_P [_ ta tb]; split; equiv_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)