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