proposition: Lemma ocon_contain_i {A} {JA: Join A} {PA: Perm_alg A} {SA: Sep_alg A}{AG : ageable A} {AA : Age_alg A}: forall P Q, Q |-- P * TT -> Q |-- ocon P Q.
proof: Proof. unfold ocon, owand, derives; simpl; intros. destruct (H a H0) as [y [z [? [? ?]]]]. exists (core y), y, z, y, a. repeat split; auto. 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