proposition: Lemma graph_tree_isomorphism_eq: forall (g: PreGraph Vertex Edge) t root, (forall v, vvalid g v -> reachable g root v) -> (graph_tree_isomorphism_v g t root <-> graph_tree_isomorphism g t).
proof: Proof. intros. split; intro; destruct H0 as [? [? ?]]; split; [ |split| |split]; intros; auto. + split; intros. - pose proof H3. destruct H4 as [? [? _]]. apply H in H4. apply H in H5. specialize (H0 s d). intuition. - rewrite <- H0 in H3. intuition. + rewrite <- H1. intuition. apply reachable_foot_valid in H3. auto. + split; intros. 1: rewrite <- H0; intuition. rewrite <- H0 in H3. pose proof H3. destruct H4 as [? [? _]]. apply H in H4. apply H in H5. intuition. + rewrite <- H1. intuition. apply reachable_foot_valid in H3; 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