proposition: Lemma eq_map_liftr n p (cs1 cs2 : seq (configuration n)) : ([seq ↑[i]_p | i <- cs1] == [seq ↑[i]_p | i <- cs2]) = (cs1 == cs2).
proof: Proof. by apply/map_eqr/cliftr_inj. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)