proposition: Lemma ocon_TT_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 ⊗ TT = P * TT.
proof: Proof. intros; apply pred_ext; hnf; intros; simpl in *; intros. + destruct_ocon H h. exists h12, h3; auto. + destruct H as [? [? [? [? ?]]]]. exists x, (core x), x0, x, x0. repeat split; auto. - apply join_comm, core_unit. - apply join_core2 in H. rewrite H. apply core_unit. Qed.
imports: VST.msl.msl_standard VST.msl.corable CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.msl_ext CertiGraph.msl_ext.sepalg