proposition: Lemma is_BinMaFin_not_evalid: forall (g1': @LGraph pSGG_Bin (@addr pSGG_Bin) (prod (@addr pSGG_Bin) LR) unit)x0 es0 e0, is_guarded_BinMaFin' (fun v => x0 <> v) (fun e => ~ In e es0) g1' -> vvalid g1' x0 -> (forall e, In e es0 -> fst e = x0) -> fst e0 = x0 -> ~ In e0 es0 -> ~ evalid g1' e0.
proof: Proof. intros. intro. destruct H as [X ?]. set (G := (Build_GeneralGraph _ _ _ (fun g => BinMaFin' (pg_lg g)) _ X: Graph')). assert (evalid G e0). 1: { simpl. rewrite Intersection_spec; auto. } pose proof @valid_graph' _ _ _ _ G _ (maGraph' _) _ H5. destruct e0. simpl in H2; subst a. rewrite (left_right_sound0' _ _ _ H5) in H6. simpl in H6. rewrite Intersection_spec in H6. destruct H6. auto. Qed.
imports: CertiGraph.lib.Ensembles_ext Coq.Lists.List VST.msl.seplog VST.msl.log_normalize VST.msl.ramification_lemmas VST.msl.Coqlib2 CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.relation_list CertiGraph.lib.Morphisms_ext CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.iter_sepcon 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 CertiGraph.graph.dag CertiGraph.graph.weak_mark_lemmas CertiGraph.graph.graph_morphism CertiGraph.graph.local_graph_copy CertiGraph.msl_application.Graph CertiGraph.msl_application.GraphBin CertiGraph.msl_application.Graph_Copy Coq.Logic.Classical