proposition: Lemma precise_wand_ewand_d {A} {JA : Join A} {PA : Perm_alg A} {SA: Sep_alg A} {CA : Canc_alg A}: forall R P Q R', precise P -> R |-- P * (Q -* R') -> Q * (ewand P R) |-- R'.
proof: Proof. intros. intro w. intros. destruct_sepcon H1 h. destruct H3 as [h3 [h4 [? [? ?]]]]. specialize (H0 h4 H5). destruct_sepcon H0 h. equate_precise_direct h3 h0. equate_canc h2 h5. apply (H7 h1); auto. Qed.
imports: VST.msl.msl_direct CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.overlapping_direct VST.msl.predicates_sa