proposition: Lemma si_src1: forall (g1 g2 : PreGraph Vertex Edge) (e: Edge), g1 ~=~ g2 -> evalid g1 e -> src g1 e = src g2 e.
proof: Proof. intros. destruct H as [? [? [? ?]]]. 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