proposition: Theorem make_listto2fold l1 l2 a c : to2it _ next l1 l2 a c = fold_left nextp (to2it _ make_list l1 l2 nil c) a.
proof: Proof. case c. now reflexivity. intros cc1 cc2 cc3; unfold to2it. repeat rewrite make_listto1fold. repeat rewrite <- fold_left_app. repeat rewrite <- app_ass. repeat rewrite <- make_listto1irA. repeat rewrite <- app_nil_end. reflexivity. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik