proposition: Lemma to1ai s l l1 p : validto1 l -> validtc4 l1 -> valid63 p -> to1i l s l1 p = false -> to1i l (to1a l s l1 p) l1 p = true.
proof: Proof. intros Hl Hl1 Hp; generalize Hl; case l; clear l Hl. intros HH; discriminate. intros o1 l _; case o1; case s; simpl; intros; apply tc4ai; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik