proposition: Lemma checkto1_all c l1 l2 p : to1all c = true -> validtc4 l1 -> validto1 l2 -> valid63 p -> to1i l2 c l1 p = true.
proof: Proof. case c; [intros HH; discriminate | idtac]. intros p1 p2 p3 Hc Hl; simpl in Hc; generalize Hc; clear Hc. case l2; try (intros; discriminate); clear l2. intros o1 l2; case l2; try (intros; discriminate). case o1; unfold to1i; intros; apply checktc4_all; auto; generalize Hc; do 3 (case tc4all; auto). Qed.
imports: PrimInt63 Cyclic63 List BasicRubik