proposition: Lemma exp_emp: forall {A B} `{ClassicalSep B} (P: A -> B), EX x:A, P x * emp = EX x: A, P x.
proof: Proof. intros. apply exp_congr. intros. rewrite sepcon_emp. 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