proposition: Theorem make_listto5irA c l1 l2 ll1 ll2 : to5it _ make_list l1 l2 (ll1++ll2) c = ll1 ++ to5it _ make_list l1 l2 ll2 c.
proof: Proof. case c; unfold to5it; auto with datatypes. intros cc1 cc2 cc3; repeat rewrite make_listto4irA; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik