proposition: Lemma sepcon_ocon_i {A}{JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG : ageable A} {AA : Age_alg A}: forall P Q, P * Q |-- P ⊗ Q.
proof: Proof. intros; hnf; intros; simpl in *; intros. destruct H as [y [z [? [? ?]]]]. remember (core z) as u. exists y, u, z, y, z. repeat split; auto. generalize (join_core H); intro. generalize (join_core (join_comm H)); intro. rewrite Hequ. replace (core z) with (core y). apply join_comm, core_unit. rewrite H2, H3; trivial. rewrite Hequ. 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