proposition: Lemma valid_step: forall (pg: PreGraph V E) {ma: MathGraph pg is_null} x y, step pg x y -> vvalid pg x /\ weak_valid pg y.
proof: Proof. intros. rewrite step_spec in H. destruct H as [? [? [? ?]]]. subst. apply valid_graph; auto. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.lib.Equivalence_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen