proposition: Lemma sepconj_assoc: forall P Q R, (P ** Q) ** R = P ** (Q ** R).
proof: Proof. intros; apply assertion_extensionality; intros; split. - intros (hx & h3 & (h1 & h2 & P1 & Q2 & EQ & DISJ) & R3 & EQ' & DISJ'). subst hx h. rewrite hunion_assoc. exists h1, (hunion h2 h3); intuition auto. exists h2, h3; intuition auto. intros l. specialize (EQ l); specialize (EQ' l). cbn in EQ'. destruct EQ as [EQ|EQ]. rewrite EQ in EQ'; auto. auto. intros l. specialize (EQ l); specialize (EQ' l). cbn in *. destruct EQ as [EQ|EQ]. auto. rewrite EQ in *. destruct (h1 l); auto. - intros (h1 & hx & P1 & (h2 & h3 & Q2 & R3 & EQ & DISJ) & EQ' & DISJ'). subst hx h. rewrite <- hunion_assoc. exists (hunion h1 h2), h3; intuition auto. exists h1, h2; intuition auto. intros l. specialize (EQ l); specialize (EQ' l). cbn in EQ'. destruct EQ' as [EQ'|EQ']. auto. destruct (h2 l); auto. intros l. specialize (EQ l); specialize (EQ' l). cbn in *. destruct EQ as [EQ|EQ]. rewrite EQ in *. destruct (h1 l); auto. auto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)