proposition: Lemma exp_FF_precise: forall {A B} `{PreciseSepLog A}, precise (EX x: B, FF).
proof: Proof. intros. rewrite exp_FF. 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