proposition: Remark aimp_sepconj: forall P P' Q, P -->> P' -> P ** Q -->> P' ** Q.
proof: Proof. intros; red. intros s h (h1 & h2 & P1 & Q2 & DISJ & EQ). exists h1, h2; auto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)