proposition: Lemma fold_right_and_True_spec: forall l, @eq (environ -> mpred) (!! fold_right_and_True_RamAssu l) (!! fold_right and True (map Prop_of_RamAssu l)).
proof: Proof. intros. apply ND_prop_ext. destruct l; [tauto |]. revert r; induction l; intros. + simpl. tauto. + change (fold_right_and_True_RamAssu (r :: a :: l)) with (Prop_of_RamAssu r /\ fold_right_and_True_RamAssu (a :: l)). change (fold_right and True (map Prop_of_RamAssu (r :: a :: l))) with (Prop_of_RamAssu r /\ fold_right and True (map Prop_of_RamAssu (a :: l))). specialize (IHl a). tauto. Qed.
imports: VST.floyd.base VST.floyd.canon VST.floyd.assert_lemmas VST.floyd.client_lemmas VST.floyd.reptype_lemmas VST.floyd.semax_tactics VST.floyd.local2ptree_denote VST.floyd.local2ptree_eval VST.floyd.call_lemmas VST.floyd.diagnosis VST.floyd.forward CertiGraph.lib.Coqlib CertiGraph.veric_ext.SeparationLogic CertiGraph.floyd_ext.ramification CertiGraph.floyd_ext.semax_ram_lemmas CertiGraph.floyd_ext.exists_trick CertiGraph.floyd_ext.closed_lemmas