proposition: Lemma Exercise1_3a6P x y: related E13_S x y <-> [/\ inc x E13_sF, inc y E13_sF & Q x = Q y].
proof: Proof. move: Exercise1_3a1 Exercise1_3a0 => gs fl. have ss: (source (second_proj E13_sF) = E13_sF) by rewrite /second_proj; aw. apply: (iff_trans (ea_relatedP fl x y)); rewrite ss. by split => [] [xs ys]; rewrite !second_proj_V. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)