proposition: Lemma canonical_ram_reduce2: forall {A: Type} s G L L' G' (Pure: A -> Prop), fold_right_sepcon_emp G |-- fold_right_sepcon_emp L * (ALL a: A, !! Pure a --> (fold_right_sepcon_emp (L' a) -* fold_right_sepcon_emp (G' a))) -> SEPx G |-- SEPx L * ModBox s (ALL a: A, !! Pure a --> (SEPx (L' a) -* SEPx (G' a))).
proof: Proof. intros. apply sepcon_EnvironBox_weaken with (ALL a : A , !!Pure a --> (SEPx (L' a) -* SEPx (G' a))). 1: { apply allp_derives; intro a. auto. } intro rho; unfold SEPx at 1 2; simpl. fold (ModBox s); rewrite go_lower_ModBox. rewrite !fold_right_sepcon_emp_spec in H. eapply derives_trans; [exact H |]. apply sepcon_derives; [apply derives_refl |]. apply allp_right; intro rho'. apply imp_andp_adjoint; apply derives_extract_prop'; intro. apply allp_derives; intro a. rewrite !fold_right_sepcon_emp_spec. auto. 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