proposition: Lemma fold_right_andp {A} `{NatDed A}: forall (l: list A) (P: A), In P l -> exists Q: A, fold_right andp TT l = P && Q.
proof: Proof. induction l; intros; simpl. 1: inversion H0. simpl in H0. destruct H0. - subst a. exists (fold_right andp TT l). reflexivity. - apply IHl in H0. destruct H0 as [QQ ?]. rewrite H0. rewrite andp_comm, andp_assoc. exists (QQ && a). reflexivity. 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