proposition: Lemma valid_path_merge: forall (g : Gph) p1 p2, paths_meet g p1 p2 -> valid_path g p1 -> valid_path g p2 -> valid_path g (p1 +++ p2).
proof: Proof. intros g p1. destruct p1 as [v1 p1]. revert v1. induction p1; intros; destruct p2 as [v p2]; unfold path_glue; unfold fst, snd. + destruct H as [v' [? ?]]. simpl in H, H2. rewrite <- H in H2. clear v' H. subst. rewrite app_nil_l. auto. + specialize (IHp1 (dst g a) (v, p2)). unfold path_glue, fst, snd in IHp1. specialize (IHp1 (paths_meet_cons _ _ _ _ _ H) (valid_path_cons _ _ _ _ H0) H1). rewrite <- app_comm_cons. destruct H0. red. split; auto. clear H1. simpl in *. destruct (p1 ++ p2) eqn:? . - destruct p1. auto. rewrite <- app_comm_cons in Heql. inversion Heql. - destruct p1; intuition. 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