proposition: Lemma allp_andp1 {A}{ND: NatDed A}: forall B (any: B) (p: B -> A) q, andp (allp p) q = (allp (fun x => andp (p x) q)).
proof: Proof. intros. apply pred_ext. apply allp_right; intro x. apply andp_derives; auto. apply allp_left with x; auto. apply andp_right. apply allp_right; intro x. apply allp_left with x. apply andp_left1; auto. apply allp_left with any. apply andp_left2; 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