fact: Definition denot (c: com) (s: store) : option store := limit (fun n => cinterp n c s) (fun i j => cinterp_mono i j c s).
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)