proposition: Lemma checktc4_all c l p : tc4all c = true -> validtc4 l -> valid63 p -> tc4i l c p = true.
proof: Proof. case c; [intros HH; discriminate | idtac]. intros p1 p2 p3 p4 Hc Hl; simpl in Hc; generalize Hc; clear Hc; case (validtc4_inv _ Hl). intros c1 (l1, (Hl1, [[H2 | [H2 | [H2 | H2]]] Hl2])); rewrite Hl1; rewrite H2; unfold tc4i; intros Hp; apply checktc5_all; auto; generalize Hp; do 4 (case tc5all; auto). Qed.
imports: PrimInt63 Cyclic63 List BasicRubik