proposition: Lemma pred_sepcon1: forall p x0, pred_sepcon (fun x => x = x0) p = p x0.
proof: Proof. intros. unfold pred_sepcon. apply pred_ext. + apply exp_left; intro l. normalize. destruct l as [| ? [|]]. - specialize (H x0); simpl in H. tauto. - specialize (H x0); simpl in H. assert (b = x0) by tauto; subst b. simpl. rewrite sepcon_emp; auto. - pose proof proj1 (H b) as HH; simpl in HH. spec HH; [auto |]. subst b. pose proof proj1 (H b0) as HH; simpl in HH. spec HH; [auto |]. subst b0. clear - H0. inversion H0; subst. simpl in H2; tauto. + apply (exp_right (x0 :: nil)). repeat apply andp_right. - apply prop_right. intros. simpl. split; [intros [? | ?]; [congruence | tauto] | left; congruence]. - apply prop_right. constructor; [simpl; tauto | constructor]. - simpl. rewrite sepcon_emp; auto. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.List_ext VST.msl.Extensionality VST.msl.simple_CCC VST.msl.seplog VST.msl.log_normalize Coq.Lists.List Coq.Sorting.Permutation Coq.Classes.Morphisms CertiGraph.msl_ext.seplog CertiGraph.msl_ext.log_normalize