proposition: Lemma Enumerable_step_list_enum: forall root l, vvalid G root -> is_tree G root -> Enumerable Vertex (reachable G root) -> step_list G root l -> Enumerable Vertex (reachable_through_set G (nodup veq_dec (filter not_null_bool l))).
proof: Proof. intros. destruct X as [l' [? ?]]. exists (remove EV root l'). split. 1: apply nodup_remove_nodup; auto. unfold Ensembles.In in *. intros. pose proof (reachable_ind.reachable_ind' _ _ _ x H H1). rewrite remove_In_iff. rewrite H3, H4, reachable_through_set_nonull_nodup. clear -MA H0 H1. intuition. destruct H as [v [? ?]]. rewrite nodup_In in H. rewrite (in_step_list_edge _ _ _ H1) in H. subst. eapply is_tree_not_to_root; eauto. 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