proposition: Lemma tc2aif3 l1 l2 ll : tc2i3 l2 ll = false -> valid3 l1 -> valid3 l2 -> l1 <> l2 -> tc2i3 l1 (tc2a3 l2 ll) = tc2i3 l1 ll.
proof: Proof. destruct l2 as ((l3, l4), p2); simpl. destruct l1 as ((l1, l2),p1); simpl. intros H1 (H2, (H3, H4)) (H5, (H6, H7)) H8. apply tc2aif; auto. case (list_eq_dec cube_dec l1 l3); auto; intros HH1. case (list_eq_dec orientation_dec l2 l4); auto; intros HH2. case (positive_dec p1 p2); auto; intros HH3. case H8; rewrite HH1, HH2, HH3; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max