proposition: Lemma math_graph_si': forall (g1 g2: PreGraph V E), g1 ~=~ g2 -> MathGraph' g1 is_null -> MathGraph' g2 is_null.
proof: Proof. intros. constructor. + intros. pose proof (proj2 (proj1 (proj2 H) _) H1). pose proof valid_graph' g1 e H2. unfold weak_valid in H3. rewrite (si_src1 _ _ _ H) in H3 by auto. rewrite !(proj1 H) in H3. auto. + intros. rewrite <- (proj1 H) in H1. apply (valid_not_null' g1 x); 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