proposition: Lemma connector_nodes (T : finType) (e1 e2 : rel T) (A B : {set T}) : forall s (p : 'I_s -> pathS (DiGraph e1)) (q : 'I_s -> pathS (DiGraph e2)), (forall i, nodes (tagged (p i)) = nodes (tagged (q i)) :> seq T) -> @connector (DiGraph e1) A B s p -> @connector (DiGraph e2) A B s q.
proof: Proof. set G1 := DiGraph e1. set G2 := DiGraph e2. move => s p q Epq [C1 C2 C3 C4]. have Spq : forall i, [set x in p i] = [set x in q i]. { move => i. apply/setP => z. by rewrite !inE !mem_path Epq. } split. - move => i /=. rewrite irredE -Epq -(@irredE G1). exact: C1. - move => i /=. rewrite -Spq C2. f_equal. move: (Epq i). case: (p i) => [[x y] pi]. case: (q i) => [[x' y'] qi]. rewrite /fst /=. rewrite !nodesE. by case. - move => i /=. rewrite -Spq C3. f_equal. move: (Epq i). case: (p i) => [[x y] pi]. case: (q i) => [[x' y'] qi]. rewrite /lst /= in pi qi *. rewrite !nodesE => [[E1 E2]]. by rewrite -(path_last pi) -(path_last qi) /= E2 E1. - move => i j /C4. by rewrite -!Spq. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)