proposition: Lemma is_tree_step_eq: forall root v1 v2 x, vvalid G root -> is_tree G root -> step G root v1 -> step G root v2 -> reachable G v1 x -> reachable G v2 x -> v1 = v2.
proof: Proof. intros. assert (reachable G root x) by (apply step_reachable with v1; auto). specialize (H0 _ H5). destruct H0 as [p [? ?]]. destruct H3 as [p1 ?]. destruct H4 as [p2 ?]. assert (forall e pa a, strong_evalid G e -> src G e = root -> dst G e = a -> G |= pa is a ~o~> x satisfying (fun _ : Vertex => True) -> G |= path_glue (root, e :: nil) pa is root ~o~> x satisfying (fun _ : Vertex => True)). { intros. apply reachable_by_path_merge with a; auto. split; split; simpl; auto. hnf. rewrite Forall_forall; intros. auto. } rewrite step_spec in H1. destruct H1 as [e1 [? [? ?]]]. rewrite step_spec in H2. destruct H2 as [e2 [? [? ?]]]. assert (strong_evalid G e1). { rewrite <- H8 in H. do 2 (split; auto). rewrite H9. apply reachable_by_path_is_reachable in H3. apply reachable_by_head_valid in H3. auto. } assert (strong_evalid G e2). { rewrite <- H10 in H. do 2 (split; auto). rewrite H11. apply reachable_by_path_is_reachable in H4. apply reachable_by_head_valid in H4. auto. } pose proof (H7 _ _ _ H12 H8 H9 H3). specialize (H7 _ _ _ H13 H10 H11 H4). apply H6 in H7. apply H6 in H14. rewrite H7 in H14. inversion H14. subst e2. rewrite H9 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