proposition: Lemma make_listtc2it3 c k ll : In k (tc2it _ make_list ll c) -> In k ll \/ (valid3 (rev3 k) /\ tc2i3 (rev3 k) c = true).
proof: Proof. intro F; case (make_listtc2i _ _ _ F); auto. intros (l3, (l4, (p, (Hp, (Hp1, (Hp2, (Hp3, Hp4))))))). right; rewrite Hp; repeat split; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max