proposition: Lemma in_step_list_edge: forall root x l, step_list G root l -> (In x (filter not_null_bool l) <-> G |= root ~> x).
proof: Proof. intros. rewrite filter_In. rewrite (H x). clear H. split; intros. + destruct H. unfold not_null_bool in H0. destruct (is_null_dec x). 1: inversion H0. pose proof H. rewrite step_spec in H1. destruct H1 as [e [? [? ?]]]. destruct (valid_graph G e H1). rewrite H2 in H4. rewrite H3 in H5. destruct H5. 1: exfalso; auto. split; auto. + destruct H as [? [? ?]]. split; auto. unfold not_null_bool. destruct (is_null_dec x); auto. exfalso. apply (valid_not_null G x); 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