proposition: Lemma iter2s_valid n : valid_triple (iter2s n).
proof: Proof. unfold iter2s; apply iter2s_aux_valid. repeat split; simpl; try (intros s HH; case HH; fail); intros s [H1 | H1]; try (case H1; fail); subst s; apply valid_state_init. Qed.
imports: ZArith List