fact: Definition aequal (a: aexp) (v: Z) : simple_assertion := fun s => aeval a s = v.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)