proposition: Lemma pred_sepcon_ocon1: forall (Q R: B -> Prop) p z (eq_dec : forall x y : B, {x = y} + {x <> y}), (forall x, Decidable (Q x)) -> (forall a, a = z \/ Q a <-> R a) -> (forall x : B, precise (p x)) -> joinable p -> p z ⊗ pred_sepcon Q p = pred_sepcon R p.
proof: Proof. intros. rewrite <- (pred_sepcon_ocon (fun x => x = z) Q R); auto. + f_equal. rewrite pred_sepcon1. auto. + intros. apply eq_dec. 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