proposition: Theorem make_listtc2irI k c ll : In k ll -> In k (tc2it _ make_list ll c).
proof: Proof. intro H; replace ll with (ll ++ nil); try rewrite make_listtc2irA; auto with datatypes. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik