fact: Definition aexists {A: Type} (P: A -> assertion) : assertion := fun (s: store) => exists (a: A), P a s.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality) CDF(IMP Sequences)