proposition: Lemma ocon_wand_d {A}{JA: Join A}{PA: Perm_alg A}: forall P Q, P ⊗ Q = EX R : pred A, (R -* P) * (R -* Q) * R.
proof: Proof. intros; apply pred_ext; hnf; intros; simpl in *. destruct_ocon H h; try_join h2 h3 h23'; equate_join h23 h23'; try_join h1 h3 h13. exists (exactly h2), h13, h2; repeat split; simpl; auto; exists h1, h3; repeat split; auto. intros h2' h12'; intros; rewrite H8 in *; equate_join h12 h12'; trivial. intros h2' h23'; intros; rewrite H8 in *; equate_join h23 h23'; trivial. destruct H as [R [w13 [w2 [? [[w1 [w3 [? [HP HQ]]]] HR]]]]]. try_join w2 w3 w23; try_join w1 w2 w12. exists w1, w2, w3, w12, w23; repeat split; auto. apply (HP w2 w12). auto. trivial. apply (HQ w2 w23); auto. Qed.
imports: CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.msl_ext VST.msl.msl_direct CertiGraph.msl_ext.sepalg