proposition: Lemma graph_match_tree_edges_in: forall s d t t', graph_match_tree_edges s d t' -> In t' (subtrees t) -> graph_match_tree_edges s d t.
proof: Proof. intros. destruct t; simpl in H0. 1: exfalso; auto. destruct H as [t1 [? ?]]. exists t1. split; auto. apply FT_succ with t'; 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