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