proposition: Lemma out_edges_step_list: forall (pg: PreGraph Vertex Edge) x es, (forall e, In e es <-> out_edges pg x e) -> (step_list pg x (map (dst pg) es)).
proof: Proof. intros. unfold step_list. intros v. split. + intros. rewrite in_map_iff in H0. destruct H0 as [e [? ?]]; subst v. apply out_edges_step. apply H; auto. + intros. rewrite step_spec in H0. destruct H0 as [e [? [? ?]]]. subst. apply in_map. rewrite H. split; auto. Qed.
imports: Coq.Logic.ProofIrrelevance CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.lib.Equivalence_ext