proposition: Lemma ocon_emp_i {A}{JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG : ageable A} {AA : Age_alg A}: forall P: pred A, P ⊗ emp = P.
proof: Proof. intros; apply pred_ext; hnf; intros; simpl in *; intros. destruct_ocon H h; try_join h2 h3 h23'; equate_join h23 h23'. rewrite (H3 _ _ (join_comm H5)) in H. generalize (join_positivity H H1); intro; rewrite H4; trivial. exists a, (core a), (core a), a, (core a). generalize (core_unit a); intro. unfold unit_for in H0. repeat split; auto. apply core_duplicable. apply core_identity. Qed.
imports: VST.msl.msl_standard VST.msl.corable CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.msl_ext CertiGraph.msl_ext.sepalg