proposition: Lemma spanning_tree_predicate_partial_si: forall (g1 g2: Graph) (e: E) (root: V) (P R: V -> Prop), Included R P -> out_edges g1 root e -> vvalid g1 root -> P root -> spanning_tree g1 (dst g1 e) R g2 -> (predicate_partialgraph g1 (fun n : V => ~ g1 |= root ~o~> n satisfying P)) ~=~ (predicate_partialgraph g2 (fun n : V => ~ g1 |= root ~o~> n satisfying P)).
proof: Proof. intros. destruct H3. apply si_stronger_partialgraph_simple with (fun n : V => ~ g1 |= dst g1 e ~o~> n satisfying R); auto. intro. unfold Ensembles.In. intros. intro. apply H5. apply reachable_by_weaken with (Q := P) in H6; auto. apply edge_reachable_by with (dst g1 e); auto. destruct H0. split; auto. split. + apply reachable_by_head_valid in H6; auto. + rewrite step_spec. exists e. 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