proposition: Lemma move_cset2 (c1 c2 : configuration k n) : all cvalid [::c1; c2] -> move rel1 c1 c2 -> (cset2 c1) != (cset2 c2) -> move rel2 (cset2 c1) (cset2 c2).
proof: Proof. rewrite /=. move=> /= /and3P[c1V c2V _] /moveP [d [dH1 dH2 dH3 dH4]] c1Dc2. have [dIsd|dNIsd] := boolP (d \in sd); last first. case/eqP: c1Dc2. apply/ffunP => i; rewrite !ffunE. apply: enum_val_inj. rewrite !enum_rankK_in ?(cvalidP _ c1V) ?(cvalidP _ c2V) ?enum_valP //. apply: dH2. apply: contra dNIsd => /eqP->. by apply: enum_valP. apply/moveP; exists (enum_rank_in dIsd d); split => /=. - rewrite !ffunE !enum_rankK_in //. by apply: rel_compat=> //; [apply: (cvalidP _ c1V) | apply: (cvalidP _ c2V)]. - move=> /= d2 dDd2. rewrite !ffunE. congr (enum_rank_in _ _). apply: dH2. rewrite -[d](enum_rankK_in dIsd) //. by apply /eqP => /enum_val_inj /eqP; rewrite (negPf dDd2). - by apply: on_top_cset2. by apply: on_top_cset2. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)