proposition: Lemma is_list_same_src_same_edge: forall root s e1 e2, is_list root -> reachable g root s -> src g e1 = s -> src g e2 = s -> evalid g e1 -> evalid g e2 -> vvalid g (dst g e1) -> vvalid g (dst g e2) -> e1 = e2.
proof: Proof. intros. assert (vvalid g s) by (apply reachable_foot_valid in H0; auto). assert (g |= (s, e1 :: nil) is s ~o~> dst g e1 satisfying (fun _ => True)) by (split; split; simpl; auto; [split; [|unfold strong_evalid; rewrite H1] | hnf; rewrite Forall_forall; intros]; auto). assert (g |= (s, e2 :: nil) is s ~o~> dst g e2 satisfying (fun _ => True)) by (split; split; simpl; auto; [split; [|unfold strong_evalid; rewrite H2] | hnf; rewrite Forall_forall; intros]; auto). destruct H0 as [ps ?]. destruct ps as [vs ps]. assert (vs = root) by (destruct H0 as [[? _] _]; simpl in H0; auto). subst vs. pose proof (reachable_by_path_merge _ _ _ _ _ _ _ H0 H8). unfold path_glue, fst, snd in H10. pose proof (reachable_by_path_is_reachable _ _ _ _ _ H10). pose proof (reachable_by_path_merge _ _ _ _ _ _ _ H0 H9). unfold path_glue, fst, snd in H12. pose proof (reachable_by_path_is_reachable _ _ _ _ _ H12). destruct H as [pf [? ?]]. apply H14 in H11. destruct H11 as [p1 [[? ?] ?]]. apply H14 in H13. destruct H13 as [p2 [[? ?] ?]]. clear H14. assert (In_path g (dst g e1) pf) by (apply In_path_Subpath with p1; auto; destruct H11 as [[_ ?] _]; apply pfoot_in; auto). assert (In_path g (dst g e2) pf) by (apply In_path_Subpath with p2; auto; destruct H13 as [[_ ?] _]; apply pfoot_in; auto). pose proof (valid_path_reachable _ _ _ _ H H14 H19). clear H11 H13 H16 H18 H14 H19. pose proof (H15 _ H10). pose proof (H17 _ H12). destruct H20. + destruct H14 as [[vx px] ?]. assert (vx = dst g e1) by (destruct H14 as [[? _] _]; simpl in H14; auto). subst vx. pose proof (reachable_by_path_merge _ _ _ _ _ _ _ H10 H14). unfold path_glue, fst, snd in H16. apply H17 in H16. rewrite H13 in H16. inversion H16. pose proof (f_equal (@length Edge) H19). rewrite !app_length in H18. simpl in H18. assert (length px = 0) by intuition. destruct px. 2: inversion H20. clear H18 H20. rewrite app_nil_r in H19. apply app_inj_tail in H19. destruct H19. auto. + destruct H14 as [[vx px] ?]. assert (vx = dst g e2) by (destruct H14 as [[? _] _]; simpl in H14; auto). subst vx. pose proof (reachable_by_path_merge _ _ _ _ _ _ _ H12 H14). unfold path_glue, fst, snd in H16. apply H15 in H16. rewrite H11 in H16. inversion H16. pose proof (f_equal (@length Edge) H19). rewrite !app_length in H18. simpl in H18. assert (length px = 0) by intuition. destruct px. 2: inversion H20. clear H18 H20. rewrite app_nil_r in H19. apply app_inj_tail in H19. destruct H19. auto. Qed.
imports: Coq.Classes.Morphisms Coq.micromega.Lia Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph