proposition: Lemma andp_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. remember (core a) as u. exists u, a, u, a, a. repeat split; try rewrite Hequ; auto; try apply core_unit; apply join_comm; 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