proposition: Lemma tc2_solve_equiv n s s1 s2 l1 l2 : valid_state s -> valid_pair (s1, s2) -> pstates_equiv (s1,s2) (l1,l2) -> solve n s s1 s2 = tc2_solve n s l1 l2.
proof: Proof. intros Hs Hg H1; generalize s Hs; elim n; simpl; auto; clear n s Hs. intros n Hrec s Hs; unfold tc2_step. rewrite (tc2_get_next_equiv s s1 s2 l1 l2); auto. generalize (tc2_get_next_movel s l1 l2); case tc2_get_next; auto. intros m Hm; rewrite Hrec; auto. apply move_valid with s; auto. apply Movel_move; auto with datatypes. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max