proposition: Lemma ocon_comm_i {A}{JA: Join A}{PA: Perm_alg A}{AG : ageable A} {AA : Age_alg A}: forall P Q, P ⊗ Q = Q ⊗ P.
proof: Proof. intros; apply pred_ext; hnf; intros; simpl in *; intros; destruct_ocon H h; exists h3, h2, h1, h23, h12; repeat split; auto; try_join h2 h3 h23'; equate_join h23 h23'; auto. Qed.
imports: VST.msl.msl_standard VST.msl.corable CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.msl_ext CertiGraph.msl_ext.sepalg