proposition: Lemma prop_forall_allp: forall (P: B -> Prop), !! (forall x, P x) = ALL x: B, !! P x.
proof: Proof. intros. apply pred_ext. + apply allp_right; intros. apply prop_derives; intros. auto. + apply allp_prop_left. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.List_ext VST.msl.Extensionality VST.msl.simple_CCC VST.msl.seplog VST.msl.log_normalize Coq.Lists.List Coq.Sorting.Permutation Coq.Classes.Morphisms CertiGraph.msl_ext.seplog CertiGraph.msl_ext.log_normalize