proposition: Lemma step_si: forall (g1 g2 : PreGraph Vertex Edge) (n n' : Vertex), g1 ~=~ g2 -> (step g1 n n' <-> step g2 n n').
proof: Proof. cut (forall (g1 g2 : PreGraph Vertex Edge) (n n' : Vertex), g1 ~=~ g2 -> step g1 n n' -> step g2 n n'). 1: intros; split; apply H; [eauto | symmetry; auto]. intros. rewrite step_spec in H0 |- *. destruct H as [? [? [? ?]]]. destruct H0 as [e [? [? ?]]]; exists e. specialize (H1 e). rewrite <- H1, <- H2, <- H3; 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