proposition: Lemma lift_aexists: forall (A: Type) (P: A -> assertion) Q, aexists P ** Q = aexists (fun x => P x ** Q).
proof: Proof. intros; apply assertion_extensionality; intros; split. - intros (h1 & h2 & (a & P1) & Q2 & DISJ & EQ). exists a, h1, h2; auto. - intros (a & h1 & h2 & P1 & Q2 & DISJ & EQ). exists h1, h2; intuition auto. exists a; auto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)