proposition: Lemma spanning_list_spanning_tree2_s: 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. inversion H3. subst. clear H3. inversion H10. subst. clear H10. inversion H11. subst. rewrite (si_edge_spanning_tree' _ g4 g2) in H7; auto. clear H3 H11. apply (spanning_bi_tree P g1 root g3 g2 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