proposition: Lemma corable_ocon_d: forall {A}{JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A} P Q, corable P -> corable Q -> corable (ocon P Q).
proof: Proof. intros. rewrite corable_spec in H, H0 |- *. unfold ocon. intros. simpl in H2 |- *. destruct H2 as [h1 [h2 [h3 [h12 [h23 [? [? [? [? ?]]]]]]]]]. exists (core y), (core y), y, (core y), y. pose proof join_core H2. pose proof join_core (join_comm H2). pose proof join_core H3. pose proof join_core (join_comm H3). pose proof join_core H4. pose proof join_core (join_comm H4). repeat split. + rewrite <- core_idem at 1. apply core_unit. + apply core_unit. + apply core_unit. + apply H with h12; auto. rewrite core_idem. congruence. + apply H0 with h23; auto. congruence. Qed.
imports: CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.msl_ext VST.msl.msl_direct CertiGraph.msl_ext.sepalg