proposition: Lemma to4aif s l1 l2 l3 l4 p1 p2 : validto4 l1 -> validto4 l2 -> validtc4 l3 -> valid63 p1 -> validtc4 l4 -> valid63 p2 -> to4i l1 s l3 p1 = false -> (l1 <> l2 \/ l3 <> l4 \/ p1 <> p2) -> to4i l2 (to4a l1 s l3 p1) l4 p2 = to4i l2 s l4 p2.
proof: Proof. intros Hl1 Hl2 Hl3 Hl4 Hp1 Hp2; generalize Hl1; case l1; clear l1 Hl1. now intros HH; discriminate. generalize Hl2; case l2; clear l2 Hl2. now intros HH; discriminate. intros o2 l2 Ho2 o1 l1 Ho1. assert (Hoo1: validto3 l1). now injection Ho1; auto. assert (Hoo2: validto3 l2). now injection Ho2; auto. case o1; case o2; case s; unfold to4i, to4a; auto; intros; rewrite to3aif; auto; try (match goal with H : _ \/ _ |- _ => case H end; auto; intros HH; left; intros HH1; case HH; rewrite HH1; auto). Qed.
imports: PrimInt63 Cyclic63 List BasicRubik