proposition: Lemma bin_graph_si: forall (g1 g2: PreGraph V E), g1 ~=~ g2 -> BinGraph g1 left_out_edge right_out_edge -> BinGraph g2 left_out_edge right_out_edge.
proof: Proof. intros. constructor. + intros. apply (bin_consist). rewrite (proj1 H); auto. + destruct H as [? [? [? ?]]]. intros. pose proof only_two_edges x e. rewrite <- H in H4. rewrite <- H1. rewrite <- H5 by auto. apply and_iff_compat_r_weak. intros. pose proof proj1 (H1 e) H6. rewrite H2 by auto. reflexivity. 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 CertiGraph.graph.MathGraph