proposition: Lemma spanning_list_spanning_tree2': forall (P: V -> Prop) g1 root g2 (e1 e2 : E), (e1 <> e2) -> (forall e, In e (e1 :: e2 :: nil) <-> out_edges g1 root e) -> vvalid g1 root -> P root -> ReachDecidable g1 (dst g1 e1) (fun x => P x /\ x <> root) -> spanning_list' (fun x => P x /\ x <> root) g1 (e1 :: e2 :: nil) g2 -> spanning_tree g1 root P g2.
proof: Proof. intros. assert (out_edges g1 root e1) by (rewrite <- H0; apply in_eq). assert (out_edges g1 root e2) by (rewrite <- H0; apply in_cons, in_eq). inversion H3. subst. destruct es. rewrite app_nil_l in H6. inversion H6. destruct es. 2: inversion H6; destruct es; inversion H12. inversion H6. subst. clear H6. inversion H7. subst. destruct es. 2: inversion H6; destruct es; inversion H13. inversion H6. subst. clear H6. inversion H8. 2: destruct es; inversion H6. rewrite <- si_edge_spanning_tree with (g1 := g1) in H12; auto. 2: destruct H4; auto. subst. clear g4 H8 H6. rename g2 into g3'. rename g3 into g2. rename g3' into g3. clear H3 H7. rename H4 into H3. rename H5 into H4. rename H12 into H5. rename H10 into H6. rewrite <- (edge_spanning_tree_equiv (fun x => P x /\ x <> root)) in H5. 2: intros; simpl; rewrite reachable_by_through_nil; intuition. simpl in H6. rewrite <- (edge_spanning_tree_equiv (fun x => (P x /\ x <> root) /\ ~ g1 |= dst g1 e1 ~o~> x satisfying (fun x0 : V => P x0 /\ x0 <> root))) in H6. 2: intros; rewrite reachable_by_through_singleton; intuition. apply (spanning_bi_tree P g1 root g2 g3 e1 e2); 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