proposition: Lemma solve_init s : valid_state s -> fold_left (fun s a => m2f a s) (solve s) s = init_state.
proof: Proof. intros Hs. apply trans_equal with (fold_left (fun s a => m2f a s) (tc2_solve 11 s s1 s2) s). apply f_equal3 with (f := @fold_left _ _). now apply refl_equal. now exact (solve_eq s). now apply refl_equal. apply tc2_solve_init. now exact s12. apply validreach11; auto. Qed.
imports: PrimInt63 List BasicRubik Rubik63