proposition: Lemma find_tree_in_leaves: forall s t1 t2, find_tree s t1 t2 -> In s (leaves t1).
proof: Proof. intros. induction H. + simpl. left; auto. + simpl. right. rewrite in_flat_map. exists tr'. split; 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