proposition: Lemma exp_FF: forall {A B} `{NatDed A}, (EX x: B, FF) = FF.
proof: Proof. intros. apply pred_ext; [| apply FF_left]. apply exp_left; intros; 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