proposition: Lemma to5ai s l l1 p : validto5 l -> validtc4 l1 -> valid63 p -> to5i l s l1 p = false -> to5i l (to5a l s l1 p) l1 p = true.
proof: Proof. intros Hl Hl1 Hp; generalize Hl; case l; clear l Hl. now intros HH; discriminate. intros o1 l Ho1; assert (validto4 l); auto. now injection Ho1; auto. case o1; case s; simpl; intros; apply to4ai; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik