proposition: Lemma rpeg_nil_inv n c p : rpeg c p = [::] -> c = `c[p] :> configuration _ n.
proof: Proof. elim: n c => [c _|n IH c] /=; first by apply/ffunP=> [] []. case: eqP => [H | H] //=; last by case: map. rewrite -{2}[c]cunliftrK. case: rpeg (IH (↓[c])) => // -> // _. by rewrite H perfect_liftr. Qed.
imports: mathcomp(all_ssreflect) hanoi(extra gdist ghanoi ghanoi3)