fact: Definition aupdate (x: ident) (a: aexp) (P: assertion) : assertion := fun s => P (update x (aeval a s) s).
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality) CDF(IMP Sequences)