proposition: Lemma tc2_get_next_equiv s s1 s2 l1 l2 : valid_state s -> valid_pair (s1, s2) -> pstates_equiv (s1,s2) (l1,l2) -> get_next s s1 s2 = tc2_get_next s l1 l2.
proof: Proof. intros Hg Hg1 H1. unfold tc2_get_next, get_next. rewrite (tc2_get_number_equiv _ _ _ _ _ Hg Hg1 H1). apply tc2_get_next_aux_equiv; auto with datatypes. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max