proposition: Lemma edge_si: forall (g1 g2 : PreGraph Vertex Edge) (n n' : Vertex), g1 ~=~ g2 -> (g1 |= n ~> n' <-> g2 |= n ~> n').
proof: Proof. intros; unfold edge in *. pose proof proj1 H n. pose proof proj1 H n'. pose proof step_si _ _ n n' H. clear - H0 H1 H2. tauto. 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