proposition: Lemma mark1_mark_list_vi: forall m1 root l m2 m3 m4 (R_DEC: forall x, In x l -> ReachDecidable g x (negateP m2)) (V_DEC: forall x, In x l -> Decidable (vvalid g x)) (R_DEC': ReachDecidable g root (negateP m1)), vvalid g root -> (negateP m1) root -> step_list g root l -> mark1 m1 root m2 -> mark_list m2 l m3 -> mark m1 root m4 -> (m3 ~=~ m4)%NodePred.
proof: Proof. intros. assert (mark m1 root m3). apply (mark_mark1_mark _ _ l m2); auto. apply (mark_func m1 root); 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