proposition: Lemma precise_exp_andp_right: forall {A B} `{PreciseSepLog A} (P Q: B -> A), precise (exp Q) -> precise (exp (P && Q)).
proof: Proof. intros. apply derives_precise with (exp Q); auto. apply exp_left; intro b; apply (exp_right b). simpl. apply andp_left2; 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