proposition: Lemma corable_local: forall P, corable (local P).
proof: Proof. intros. simpl; intros. unfold local, lift1. apply corable_prop. Qed.
imports: CertiGraph.lib.Equivalence_ext CertiGraph.veric_ext.SeparationLogic VST.floyd.base VST.floyd.client_lemmas VST.floyd.assert_lemmas VST.floyd.closed_lemmas VST.floyd.forward_lemmas