proposition: Lemma valid_path_reachable: forall g p v1 v2, valid_path g p -> In_path g v1 p -> In_path g v2 p -> reachable g v1 v2 \/ reachable g v2 v1.
proof: Proof. intros. assert (g |= p is (phead p) ~o~> (pfoot g p) satisfying (fun _ => True)) by (split; split; simpl; auto; rewrite path_prop_equiv; intros; auto). destruct (reachable_by_path_split_in _ _ _ _ _ _ H2 H0) as [p1 [p2 [? [? ?]]]]. rewrite H3 in H1. apply In_path_glue in H1. destruct H1. + right. apply (reachable_path_in' _ _ _ _ H4); auto. + left. apply (reachable_path_in _ _ _ _ H5); 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