proposition: Lemma ocon_andp_prop_d {A}{JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}: forall P Q R, P ⊗ (!!Q && R) = !!Q && (P ⊗ R).
proof: Proof. intros; apply pred_ext; hnf; intros; simpl in *. + destruct H as [h1 [h2 [h3 [h12 [h23 [? [? [? [? [? ?]]]]]]]]]]. split; auto. exists h1, h2, h3, h12, h23. intuition. + destruct H as [? [h1 [h2 [h3 [h12 [h23 [? [? [? [? ?]]]]]]]]]]. exists h1, h2, h3, h12, h23. unfold andp. intuition. Qed.
imports: CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.msl_ext VST.msl.msl_direct CertiGraph.msl_ext.sepalg