proposition: Lemma closed_wrt_wand: forall (S : ident -> Prop) (P Q : environ -> mpred), closed_wrt_vars S P -> closed_wrt_vars S Q -> closed_wrt_vars S (P -* Q).
proof: Proof. intros; hnf in *; intros. simpl. f_equal; eauto. Qed.
imports: VST.floyd.base VST.floyd.assert_lemmas VST.floyd.client_lemmas