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