proposition: Lemma cvalidP (c : configuration k n) : reflect (forall i, i \in sd -> c i \in sp) (cvalid c).
proof: Proof. apply: (iffP forallP) => [H d|H d]; first by have /implyP := H d. by apply/implyP/H. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)