proposition: Lemma correspondences_P x y z: inc z (correspondences x y) <-> [/\ correspondence z, source z = x & target z = y].
proof: Proof. rewrite /correspondence /source/target. split. by case/setX_P => [pz /setP_P spz/setX_P [p_qz /set1_P -> /set1_P ->]]. move => [ [ [tp sgp] aux] <- <-]. apply:setX_i;[ exact | by apply/ setP_P | apply:setX_i; fprops]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)