proposition: Lemma allp_andp2 {A}{ND: NatDed A}: forall B (any: B) p (q: B -> A), andp p (allp q) = (allp (fun x => andp p (q x))).
proof: Proof. intros. rewrite andp_comm. rewrite allp_andp1; auto. f_equal. extensionality x. rewrite andp_comm; auto. Qed.
imports: VST.floyd.base2 VST.floyd.client_lemmas VST.floyd.closed_lemmas VST.floyd.nested_pred_lemmas VST.floyd.nested_field_lemmas VST.floyd.efield_lemmas VST.floyd.mapsto_memory_block VST.floyd.reptype_lemmas VST.floyd.data_at_rec_lemmas VST.floyd.field_at VST.floyd.nested_loadstore VST.floyd.entailer