fact: Fixpoint valid_N (l: addr) (sz: nat) : assertion := match sz with O => emp | S sz => valid l ** valid_N (l + 1) sz end.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)