proposition: Lemma is_tree_not_to_root: forall root v x, is_tree G root -> G |= root ~> v -> reachable G v x -> x <> root.
proof: Proof. intros. destruct H0 as [? [? ?]]. assert (reachable G root root) by (apply reachable_refl; auto). specialize (H _ H4). destruct H as [p [? ?]]. assert (G |= (root, nil) is root ~o~> root satisfying (fun _ => True)) by (split; split; simpl; auto; red; simpl; split; intros; auto). pose proof (H5 _ H6). intro. subst x. destruct H1 as [path' ?]. rewrite step_spec in H3. destruct H3 as [e [? [? ?]]]. assert (G |= (root, e :: nil) is root ~o~> v satisfying (fun _ => True)) by (split; split; simpl; intuition; hnf; [subst root v | rewrite Forall_forall; intros]; auto). pose proof (reachable_by_path_merge _ _ _ _ _ _ _ H10 H1). specialize (H5 _ H11). rewrite H7 in H5. clear -H5. destruct path' as [v' p']. unfold path_glue in H5. simpl in H5. inversion H5. 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