fact: Definition prog2 := ASSIGN "x" (CONST 0) ;; ASSIGN "y" (CONST 0) ;; WHILE (LESSEQUAL (VAR "x") (CONST 1000)) (ASSIGN "y" (VAR "x") ;; ASSIGN "x" (PLUS (VAR "x") (CONST 1))).
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)