proposition: Lemma states_equiv_equiv ss1 ss2 ll : states_equiv ss1 ll -> lequiv ss1 ss2 -> states_equiv ss2 ll.
proof: Proof. unfold states_equiv, lequiv; intros H1 H2 s. apply iff_trans with (1 := H1 s). repeat rewrite in_map_iff; split; intros (x, (Hx1, Hx2)); exists x; try (rewrite H2); auto; rewrite <- H2; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max