proposition: Lemma gen_dst_preserve_math: forall (g: PreGraph V E) e t (M: MathGraph g is_null), weak_valid g t -> MathGraph (pregraph_gen_dst g e t) is_null.
proof: Proof. intros. refine (Build_MathGraph (pregraph_gen_dst g e t) is_null _ (valid_not_null g)). simpl. intros. apply (valid_graph g) in H0. destruct H0. split. + auto. + unfold updateEdgeFunc. destruct_eq_dec e e0. - apply H. - apply H1. Defined.
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