proposition: Lemma lift_simple_conj: forall P Q R, (P //\\ Q) ** R = P //\\ (Q ** R).
proof: Proof. intros; apply assertion_extensionality; intros; split. - intros (h1 & h2 & (P1 & Q1) & R2 & DISJ & EQ). split; auto. exists h1, h2; auto. - intros (P1 & (h1 & h2 & Q1 & R2 & DISJ & EQ)). exists h1, h2; intuition auto. split; auto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)