proposition: Lemma move_liftln m n (c1 c2 : configuration q m) : move r2 (cliftln n p (plift p c1)) (cliftln n p (plift p c2)) = move r1 c1 c2.
proof: Proof. apply/idP/idP=> H; last first. apply: move_mergel_inv => //. - by apply: cdisjoint_plift_perfect. - by apply: cdisjoint_plift_perfect. by rewrite (@plift_move _ _ _ r1). have := move_mergel r2Irr H. by rewrite (@plift_move _ _ _ r1). Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)