proposition: Lemma si_edge_spanning_tree: forall (g1 g2 g3: Graph) (e: E) (P: V -> Prop), g1 ~=~ g2 -> evalid g1 e -> (edge_spanning_tree g1 e P g3 <-> edge_spanning_tree g2 e P g3).
proof: Proof. cut (forall g1 g2 g3 e P, g1 ~=~ g2 -> evalid g1 e -> edge_spanning_tree g1 e P g3 -> edge_spanning_tree g2 e P g3); intros. + split; intros; [apply H with g1 | apply H with g2]; auto. - symmetry; auto. - destruct H0 as [_ [? _]]. specialize (H0 e). intuition. + assert (dst g1 e = dst g2 e). { destruct H as [_ [? [_ ?]]]. specialize (H e). specialize (H2 e). rewrite <- H2; intuition. } destruct H1 as [[? ?] | [? ?]]; [left | right]; split; [rewrite <- H2 .. |]; auto. - rewrite <- (si_spanning_tree g1); auto. - destruct H as [? [? [? ?]]]. destruct H3 as [? [? [? [? ?]]]]. split; [|split; [|split; [|split]]]; intros. * specialize (H v). specialize (H3 v). intuition. * specialize (H4 e0). specialize (H7 e0 H11). intuition. * specialize (H7 e0 H11). specialize (H5 e0). specialize (H8 e0 H11). rewrite H5 in H8; intuition. * specialize (H7 e0 H11). specialize (H6 e0). specialize (H9 e0 H11). rewrite H6 in H9; intuition. * destruct H10; [left | right]; auto. intuition. rewrite <- H10. symmetry. specialize (H4 e). apply H5; intuition. Qed.
imports: Coq.Classes.Morphisms CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2 CertiGraph.graph.reachable_ind Coq.Logic.Classical