proposition: Lemma si_trans: forall (G1 G2 G3: PreGraph Vertex Edge), G1 ~=~ G2 -> G2 ~=~ G3 -> G1 ~=~ G3.
proof: Proof. intros; destruct H as [? [? [? ?]]], H0 as [? [? [? ?]]]. split; [| split; [| split]]; intros; [firstorder | firstorder | |]; specialize (H1 e); specialize (H2 e); specialize (H3 e); specialize (H4 e); specialize (H5 e); specialize (H6 e); assert (evalid G2 e) by (apply H1; auto); specialize (H2 H7 H9); specialize (H3 H7 H9); specialize (H5 H9 H8); specialize (H6 H9 H8); congruence. 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