proposition: Lemma path_liftr n p (c : configuration n) (cs : seq (configuration _)) : path move ↑[c]_p [seq ↑[i]_p | i <- cs] = path move c cs.
proof: Proof. by apply: (@path_merger 1). Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)