proposition: Lemma iter_equiv n : pstates_equiv (iters n) (iter n).
proof: Proof. unfold iters, iter. apply iter_aux_equiv; simpl; auto. now split; intros s [H | H]; try (case H; fail); subst; apply valid_state_init. split; red; simpl fst; simpl snd. replace (tc2it _ make_list nil s0) with (map (fun x => rev3 (encode_state x)) (init_state :: nil)). now intros s; split; auto. now apply refl_equal. replace (tc2it _ make_list nil s0) with (map (fun x => rev3 (encode_state x)) (init_state :: nil)). now intros s; split; auto. apply refl_equal. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max