proposition: Lemma mark1_exists: forall m x, vvalid g x -> {m': NodePred V | mark1 m x m'}.
proof: Proof. intros. destruct ((node_pred_dec m) x). + exists m. split; auto. split; [exact a |]. intros; reflexivity. + assert (forall y, {y = x \/ m y} + {~ (y = x \/ m y)}). 1: { intros. apply sumbool_dec_or. + apply equiv_dec. + apply node_pred_dec. } exists (existT _ (fun y => y = x \/ m y) X). split. * auto. * split; [simpl; auto |]. intros; simpl. assert (n' <> x) by congruence. tauto. 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