proposition: Lemma mark_list_marked: forall m1 l m2 (R_DEC: forall x, In x l -> ReachDecidable g x (negateP m1)) (V_DEC: forall x, In x l -> Decidable (vvalid g x)), mark_list m1 l m2 -> forall n : V, m1 n -> m2 n.
proof: Proof. apply (ind_RV_DEC (fun m1 l m2 => forall n : V, m1 n -> m2 n)). + intros. rewrite <- (H n). auto. + intros. apply H. apply (mark_markeds m v m'); auto. apply R_DEC; left; auto. Qed.
imports: Coq.Logic.ProofIrrelevance CertiGraph.lib.Ensembles_ext Coq.Lists.List Coq.Classes.Morphisms CertiGraph.lib.Coqlib CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext VST.msl.Coqlib2 CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_computable CertiGraph.graph.reachable_ind CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2