proposition: Lemma is_list_edge_src_the_same: forall root s d v, vvalid G root -> is_list root -> reachable G root s -> reachable G root v -> G |= s ~> d -> G |= v ~> d -> s = v.
proof: Proof. intros. destruct H3 as [? [? ?]]. rewrite step_spec in H6. destruct H6 as [es [? [? ?]]]. destruct H4 as [? [? ?]]. rewrite step_spec in H10. destruct H10 as [ev [? [? ?]]]. assert (G |= (s, es :: nil) is s ~o~> d satisfying (fun _ => True)). { split; split; simpl; auto; [unfold strong_evalid; rewrite H7, H8; split; auto | hnf; rewrite Forall_forall; intros; auto]. } assert (G |= (v, ev :: nil) is v ~o~> d satisfying (fun _ => True)). { split; split; simpl; auto; [unfold strong_evalid; rewrite H11, H12; split; auto | hnf; rewrite Forall_forall; intros; auto]. } destruct H1 as [[vs ps] ?]. destruct H2 as [[vv pv] ?]. pose proof (reachable_by_path_merge _ _ _ _ _ _ _ H1 H13). unfold path_glue, fst, snd in H15. pose proof (reachable_by_path_merge _ _ _ _ _ _ _ H2 H14). unfold path_glue, fst, snd in H16. destruct H0 as [pf [? ?]]. pose proof (reachable_by_path_is_reachable _ _ _ _ _ H16). apply H17 in H18. destruct H18 as [pp [[? ?] ?]]. apply H19 in H15. apply H19 in H16. rewrite H15 in H16. inversion H16. apply app_inj_tail in H23. destruct H23. subst es. rewrite H7 in H11. auto. Qed.
imports: Coq.Arith.Arith CertiGraph.lib.Coqlib CertiGraph.lib.EnumEnsembles CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.MathGraph CertiGraph.graph.FiniteGraph CertiGraph.graph.reachable_computable Coq.Lists.List