proposition: Theorem make_listtc6irA c l1 l2 ll1 ll2 : tc6it _ make_list l1 l2 (ll1 ++ ll2) c = ll1 ++ tc6it _ make_list l1 l2 ll2 c.
proof: Proof. case c; unfold tc6it; auto with datatypes. intros cc1 cc2 cc3 cc4 cc5 cc6; repeat rewrite make_list63irA. reflexivity. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik