fact: Fixpoint hinit (l: addr) (sz: nat) (h: heap) : heap := match sz with O => h | S sz => hupdate l 0 (hinit (l + 1) sz h) end.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)