proposition: Lemma subgraph_step: forall (g: Graph) (p: V -> Prop) x y, step g x y -> p x -> p y -> step (predicate_subgraph g p) x y.
proof: Proof. intros. rewrite step_spec in H |- *. destruct H as [e [? [? ?]]]. exists e. split; [| split; simpl; auto]. simpl. unfold predicate_evalid. rewrite H2, H3. auto. Qed.
imports: Coq.Logic.ProofIrrelevance Coq.Sets.Ensembles Coq.Sets.Finite_sets Coq.Classes.Morphisms CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.relation_list CertiGraph.lib.List_ext CertiGraph.lib.Equivalence_ext CertiGraph.lib.EquivDec_ext VST.msl.Coqlib2 Coq.Lists.List CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_ind