proposition: Lemma loop2 i j body : body (i + j) = abortT tt -> for_loop (i + j).+1 i body = Ret tt.
proof: Proof. move=> Hbody /=. case : ifPn => Hcond. - reflexivity. - by rewrite Hbody /= /abortT. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib ifail_lib istate_lib