proposition: Lemma path_liftln m n (c : configuration q m) (cs : seq (configuration _ _)) : path (move r2) (cliftln n p (plift p c)) (map (cliftln n p \o (plift p)) cs) = path (move r1) c cs.
proof: Proof. by elim: cs c => //= c1 cs1 IH c; rewrite move_liftln IH. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)