proposition: Lemma edge_spanning_tree_inj: forall g1 root g2, edge_spanning_tree g1 root g2 <-> (marked_reachable g1 (dst g1 root) g2 /\ SIMPLE_SPANNING_TREE.edge_spanning_tree g1 root (unmarked g1) g2).
proof: Proof. intros. split; intro. + hnf in H. destruct (node_pred_dec (marked g1) (dst g1 root)). - destruct H. split; [| right]; intros; auto. intro y. assert (~ g1 |= dst g1 root ~o~> y satisfying (unmarked g1)); [| firstorder]. intro. apply reachable_by_head_prop in H1. unfold unmarked in H1. rewrite negateP_spec in H1. exfalso; auto. - rewrite spanning_tree_inj in H. destruct H. split; auto. left. auto. + destruct H. hnf. destruct (node_pred_dec (marked g1) (dst g1 root)); destruct H0 as [[? ?] | [? ?]]. - unfold unmarked in H0. rewrite negateP_spec in H0. exfalso; auto. - split; auto. intro v; specialize (H v). assert (~ g1 |= dst g1 root ~o~> v satisfying (unmarked g1)); [| tauto]. intro. apply reachable_by_head_prop in H2. unfold unmarked in H2. rewrite negateP_spec in H2. exfalso; auto. - rewrite spanning_tree_inj. auto. - exfalso; 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