proposition: Lemma loop1 i j body : for_loop (i.+1 + j) i body = (body (i + j)) (fun _ => for_loop (i + j) i body).
proof: Proof. rewrite /=. by case : ifPn ; rewrite ltnNge leq_addr. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib ifail_lib istate_lib