fact: Definition contains (l: addr) (v: Z) : assertion := fun s h => h = hupdate l v hempty.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)