proposition: Lemma si_sym: forall (G1 G2: PreGraph Vertex Edge), G1 ~=~ G2 -> G2 ~=~ G1.
proof: Proof. intros; destruct H as [? [? [? ?]]]; split; [| split; [| split]]; auto; firstorder. 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