proposition: Lemma make_listtc2ir3 c l ll : valid3 (rev3 l) -> tc2i3 (rev3 l) c = true -> In l (tc2it _ make_list ll c).
proof: Proof. destruct l as ((l1,l2),p1); simpl. intros (H1, (H2, H3)) H5. apply make_listtc2ir; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max