proposition: Lemma configuration1_eq (c1 c2 : configuration 1) : (c1 == c2) = (c1 sdisk == c2 sdisk).
proof: Proof. apply/eqP/eqP; first by move=> /ffunP/(_ sdisk). by move=> H; apply/ffunP=> i; rewrite [i]disk1_all. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)