proposition: Lemma allp_derives': forall {A B} `{NatDed A} (P Q : B -> A), P |-- Q -> allp P |-- allp Q.
proof: Proof. intros; apply allp_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