proposition: Theorem make_list63fold l1 l2 a c : int63it _ next l1 l2 a c = fold_left nextp (int63it _ make_list l1 l2 nil c) a.
proof: Proof. rewrite int63it_naive; unfold make_list. rewrite int63it_naive; unfold naive_int63it. generalize l1 l2 a c; clear l1 l2 a c. generalize (1%positive); elim 62%nat. intros p l1 l2 a c; repeat rewrite naive_aux0. now case int63i; auto. intros n Hrec p l1 l2 a c. repeat rewrite naive_auxS. case int63i; auto. simpl. rewrite Hrec. replace ((l1,l2,p) :: nil) with (((l1,l2,p) :: nil)++nil); auto with datatypes. rewrite (naive_auxA ((l1,l2,p) :: nil)); auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik