proposition: Lemma checktc2_all c l1 l2 p : tc2all c = true -> validtc2 l1 -> validto5 l2 -> valid63 p -> tc2i l1 l2 p c = true.
proof: Proof. case c; [intros HH; discriminate | idtac]. intros p1 p2 Hc Hl; simpl in Hc; generalize Hc; clear Hc; case (validtc2_inv _ Hl). intros c1 [l3 [Hl1 [[H2 | H2] Hl2]]]; rewrite Hl1; rewrite H2; unfold tc4i; intros Hp; apply checkto5_all; auto; generalize Hp; do 3 (case to5all; auto). Qed.
imports: PrimInt63 Cyclic63 List BasicRubik