proposition: Lemma forest_head_in_leaves: forall d t, In d (forest_head (subtrees t)) -> In d (leaves t).
proof: Proof. intros. induction t. 1: simpl in H; exfalso; auto. simpl in H. simpl. right. induction l. + simpl in H. exfalso; auto. + simpl in *. destruct a. - specialize (IHl H). simpl. auto. - simpl in *. destruct H; [left | right]; auto. specialize (IHl H). apply in_or_app. right; 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