proposition: Lemma insert_local': forall Q1 Q R, local (locald_denote Q1) && (LOCALx Q R) = LOCALx (Q1 :: Q) R.
proof: Proof. intros. extensionality rho. unfold LOCALx, local; super_unfold_lift. simpl. apply pred_ext; autorewrite with gather_prop; normalize; decompose [and] H; clear H. 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