proposition: Lemma disj_comm_i {A: Type} {JA: Join A} {PA: Perm_alg A} {AG : ageable A}: forall P Q, disjointed P Q -> disjointed Q P.
proof: Proof. unfold disjointed; intros. specialize (H h3 h2 h1 h23 h12). do 2 (spec H; [apply join_comm; auto |]). do 2 (spec H; [auto |]). destruct H; split; auto. apply joins_comm; auto. Qed.
imports: VST.msl.msl_standard VST.msl.corable CertiGraph.msl_ext.ramify_tactics CertiGraph.msl_ext.msl_ext CertiGraph.msl_ext.sepalg