proposition: Lemma binGraph_out_edges (pg: PreGraph V E) (bi: BinGraph pg left_out_edge right_out_edge): forall x e, vvalid pg x -> (In e (left_out_edge x :: right_out_edge x :: nil) <-> out_edges pg x e).
proof: Proof. intros. unfold out_edges. simpl. pose proof only_two_edges x e H. firstorder; subst; tauto. 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