proposition: Lemma In_path_si: forall (g1 g2: Gph) p x, g1 ~=~ g2 -> valid_path g1 p -> (In_path g1 x p <-> In_path g2 x p).
proof: Proof. cut (forall g1 g2 p x, g1 ~=~ g2 -> valid_path g1 p -> In_path g1 x p -> In_path g2 x p); intros. + split; intros; [apply H with g1 | apply H with g2]; auto. 1: symmetry; auto. apply valid_path_si with g1; auto. symmetry; auto. + destruct p as [v p]. unfold In_path in *. simpl in H1 |-* . destruct H1; [left | right]; auto. destruct H1 as [e [? ?]]. exists e. split; auto. destruct (valid_path_strong_evalid _ _ _ _ H0 H1) as [? [? ?]]. destruct H as [? [? [? ?]]]. specialize (H6 e). assert (src g1 e = src g2 e) by (apply H7; intuition). assert (dst g1 e = dst g2 e) by (apply H8; intuition). rewrite <- H9, <- H10. auto. Qed.
imports: Coq.Logic.ProofIrrelevance Coq.micromega.Lia CertiGraph.lib.Coqlib CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext CertiGraph.graph.graph_model Coq.Lists.List Coq.Lists.ListDec