proposition: Lemma weak_derives_strong: forall (P Q: mpred), P |-- Q -> P |-- (weak_derives P Q && emp) * P.
proof: Proof. intros. cancel. apply andp_right. 2: cancel. assert (HS: emp |-- TT) by entailer; sep_apply HS; clear HS. apply derives_weak. assumption. Qed.
imports: CertiGraph.CertiGC(env_graph_gc gc_spec) CertiGraph.msl_ext.ramification_lemmas VST.concurrency.conclib