proposition: Lemma sepconj_comm: forall P Q, P ** Q = Q ** P.
proof: Proof. assert (forall P Q s h, (P ** Q) s h -> (Q ** P) s h). { intros P Q s h (h1 & h2 & P1 & Q2 & EQ & DISJ); subst h. exists h2, h1; intuition auto. apply hdisjoint_sym; auto. symmetry; apply hunion_comm; auto. } intros; apply assertion_extensionality; intros; split; auto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)