proposition: Lemma precise_prop_andp: forall {A} `{PreciseSepLog A} P Q, (P \/ ~ P) -> (P -> precise Q) -> precise (!!P && Q).
proof: Proof. intros. destruct H0. + apply precise_andp_right. auto. + apply precise_andp_left. apply derives_precise with FF; [| apply FF_precise]. apply prop_derives; auto. 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