proposition: Lemma si_edge_spanning_tree': forall (g1 g2 g3: Graph) (e: E) (P: V -> Prop), g2 ~=~ g3 -> (edge_spanning_tree g1 e P g2 <-> edge_spanning_tree g1 e P g3).
proof: Proof. cut (forall g1 g2 g3 e P, g2 ~=~ g3 -> edge_spanning_tree g1 e P g2 -> edge_spanning_tree g1 e P g3); intros. + split; intros; [apply H with g2 | apply H with g3]; auto. symmetry; auto. + destruct H0 as [[? ?] | [? ?]]; [left | right]; split; auto. - rewrite <- (si_spanning_tree' _ _ _ _ _ H); auto. - destruct H as [? [? [? ?]]]. destruct H1 as [? [? [? [? ?]]]]. split; [|split; [|split; [|split]]]; intros. * specialize (H v). specialize (H1 v). intuition. * specialize (H2 e0). specialize (H5 _ H9). intuition. * specialize (H2 e0). assert (evalid g2 e0) by intuition. specialize (H3 _ H12 H11). specialize (H6 _ H9 H10 H12). rewrite <- H3. rewrite H6. auto. * specialize (H2 e0). assert (evalid g2 e0) by intuition. specialize (H4 _ H12 H11). specialize (H7 _ H9 H10 H12). rewrite <- H4. rewrite H7. auto. * destruct H8 as [? | [? [? ?]]]; [left | right]. rewrite <- H2. auto. specialize (H2 e). assert (evalid g3 e) by intuition. specialize (H4 _ H10 H11). specialize (H3 _ H10 H11). rewrite <- H4. rewrite <- H3. rewrite H9. rewrite <- H. auto. 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