proposition: Lemma path_cset2 (c : configuration _ _) cs : all cvalid (c :: cs) -> path (move rel1) c cs -> path (move rel2) (cset2 c) (rm_rep (cset2 c) [seq (cset2 i) | i <- cs]).
proof: Proof. elim: cs c => //= c1 cs IH c => /and3P[c1V c2V c3V] /andP[cMc1 c1Pcs]. case: eqP => [->|/eqP cDc1 /=]; first by apply: IH; rewrite ?c2V. rewrite move_cset2 => //=; first by apply: IH; rewrite ?c2V. by rewrite c1V c2V. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)