proposition: Lemma binE_only2 (pg : PreGraph V E) {bi: BinGraph pg left_out_edge right_out_edge} : forall v v1 v2 n, vvalid pg v -> binE pg v = (v1 ,v2) -> (step pg v n <-> n = v1 \/ n = v2).
proof: Proof. intros; unfold binE in H. split; intros. + inversion H1; subst. inversion H0; subst. assert (e = left_out_edge (src pg e) \/ e = right_out_edge (src pg e)) by (rewrite <- only_two_edges; eauto). destruct H3; rewrite <- H3; auto. + rewrite step_spec; inversion H0; subst. destruct H1; [exists (left_out_edge v) | exists (right_out_edge v)]; subst. - split; [| split]; [eapply left_valid | rewrite left_sound |]; eauto. - split; [| split]; [eapply right_valid | rewrite right_sound |]; eauto. 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