proposition: Lemma corable_andp_ocon1_d {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}: forall P Q R, corable P -> ocon (P && Q) R = P && (ocon Q R).
proof: Proof. intros. apply pred_ext. + intros h [h1 [h2 [h3 [h12 [h23 [? [? [? [[? ?] ?]]]]]]]]]. split. - apply join_core in H2. rewrite corable_spec in H. apply H with h12; [congruence | auto]. - exists h1, h2, h3, h12, h23. tauto. + intros h [? [h1 [h2 [h3 [h12 [h23 [? [? [? [? ?]]]]]]]]]]. exists h1, h2, h3, h12, h23. rewrite corable_spec in H. repeat split; auto. apply join_core in H3. apply H with h; [congruence | auto]. Qed.
imports: CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.msl_ext VST.msl.msl_direct CertiGraph.msl_ext.sepalg