proposition: Lemma precise_ocon_self {A} {JA: Join A} {PA: Perm_alg A} {SA: Sep_alg A} {AG : ageable A} {AA : Age_alg A} {DA: Disj_alg A}: forall P, precise P -> P = ocon P P.
proof: Proof. intros. apply pred_ext. - apply ocon_contain_i. repeat intro. destruct (join_ex_identity a) as [e [? ?]]. red in u. apply join_comm in u. exists a, e. split; auto. - repeat intro. destruct_ocon H0 a. try_join a2 a3 a23'. equate_join a23 a23'. equate_precise a12 a23. assert (identity a1). { assertSub a1 a12 H5. eapply join_sub_joins_identity; eauto. } apply H4 in H0. subst. assert (identity a3). { assertSub a3 a12 H0. eapply join_sub_joins_identity; eauto. } apply join_comm in H2. apply H0 in H2. now subst. Qed.
imports: VST.msl.msl_standard VST.msl.corable CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.msl_ext CertiGraph.msl_ext.sepalg