fact: Record heap : Type := { contents :> addr -> option Z; isfinite : exists i, forall j, i <= j -> contents j = None }.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)