proposition: Lemma vertex_update_mark1: forall (g1: Graph) x (g2: Graph), g1 ~=~ g2 -> vvalid g1 x -> unmarked g1 x -> vlabel g2 x = label_mark (vlabel g1 x) -> (forall y, x <> y -> vlabel g2 y = vlabel g1 y) -> (forall e, elabel g2 e = elabel g1 e) -> mark1 g1 x g2.
proof: Proof. intros. split; [| split; [| split]]; auto. + simpl. rewrite H2. apply label_mark_sound. apply H1. + intros y HH; specialize (H3 y HH). clear - H3. simpl. rewrite H3. reflexivity. 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