proposition: Lemma ext_to_prod_rel_V r r' x x': equivalence r -> equivalence r' -> inc x (substrate r) -> inc x' (substrate r') -> Vf (ext_to_prod(canon_proj r)(canon_proj r')) (J x x') = J (class r x) (class r' x').
proof: Proof. move=> er er' xs xs'. by rewrite ext_to_prod_V; aww; rewrite !canon_proj_V. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)