proposition: Lemma tc4ai s l p : validtc4 l -> valid63 p -> tc4i l s p = false -> tc4i l (tc4a l s p) p = true.
proof: Proof. intros H Hp. assert (Hp1: (Zpos p <= 63)%Z); auto. case (validtc4_inv _ H); clear H. intros p1 [l1 [H1 [[H2 | [H2 | [H2 | H2]]] H3]]]; rewrite H1; rewrite H2; clear H1 H2; case s; unfold tc4i, tc4a; auto; intros; apply tc5ai; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik