proposition: Lemma precise_exp_prop_andp: forall {A B} `{PreciseSepLog A} (P: B -> Prop) (Q: B -> A), ((exists x, P x) \/ (~ exists x, P x)) -> (forall x, precise (Q x)) -> (forall x y, P x -> P y -> Q x = Q y) -> precise (EX x: B, !! P x && Q x).
proof: Proof. intros. destruct H0 as [[x ?] | ?]. + apply derives_precise with (Q x). - apply exp_left; intro y. normalize. pose proof H2 _ _ H0 H3. rewrite H4; auto. - apply H1. + apply derives_precise with FF. - normalize; intros x ?. specialize (H0 (ex_intro _ x H3)); tauto. - apply FF_precise. Qed.
imports: VST.msl.Extensionality VST.msl.simple_CCC VST.msl.seplog VST.msl.log_normalize Coq.Lists.List CertiGraph.msl_ext.seplog CertiGraph.msl_ext.abs_addr