proposition: Lemma path_unlift_eq n (c : configuration n.+1) (cs : seq (configuration _)) : (forall c1, c1 \in cs -> c1 ldisk = c ldisk)-> path move ↓[c] [seq ↓[i] | i <- cs] = path move c cs.
proof: Proof. move=> H. rewrite -(@path_liftr _ (c ldisk)). rewrite cunliftrK -map_comp. congr path. elim: cs H => //= a cs IH H. rewrite -{1}(H a). by rewrite cunliftrK IH // => v Hv; apply: H; rewrite inE orbC Hv. by rewrite inE eqxx. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)