proposition: Lemma path_unlift n (c : configuration n.+1) (cs : seq (configuration _)) : path move c cs -> path move ↓[c] (rm_rep ↓[c] [seq ↓[i] | i <- cs]).
proof: Proof. by move=> H; apply: path_crshift. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)