proposition: Lemma ocon_precise_elim_d {A}{JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{CA: Canc_alg A}{DA : Disj_alg A}: forall P : pred A, precise P -> P ⊗ P = P.
proof: Proof. intros; apply pred_ext; intro w; intro. destruct_ocon H0 h. try_join h2 h3 h23'; equate_join h23 h23'. equate_precise_direct h12 h23. assert (emp h1). assertSub h1 h12 HS. assert (joins h1 h12). exists w; auto. apply (join_sub_joins_identity HS H4). equate_canc h1 h3. apply (join_unit1_e _ _ H4) in H6. subst. auto. hnf. exists (core w), w, (core w), w, w. split. apply core_unit. split. apply join_comm, core_unit. split. apply join_comm, core_unit. split; auto. Qed.
imports: CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.msl_ext VST.msl.msl_direct CertiGraph.msl_ext.sepalg