proposition: Lemma si_refl: forall (G : PreGraph Vertex Edge), G ~=~ G.
proof: Proof. intros; repeat split; auto. 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