proposition: Lemma out_edges_si: forall (g1 g2 : PreGraph Vertex Edge) (v: Vertex) (e : Edge), g1 ~=~ g2 -> (out_edges g1 v e <-> out_edges g2 v e).
proof: Proof. cut (forall (g1 g2: PreGraph Vertex Edge) v e, g1 ~=~ g2 -> out_edges g1 v e -> out_edges g2 v e). + intros. split; intros; [apply (H g1) | apply (H g2)]; auto. symmetry; auto. + intros. destruct H0. destruct H as [_ [? [? _]]]. specialize (H e). specialize (H2 e). split; [|rewrite <- H2]; intuition. Qed.
imports: Coq.Logic.ProofIrrelevance CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.lib.Equivalence_ext