fact: Definition aimp (P Q: assertion) : Prop := forall s h, P s h -> Q s h.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)