proposition: Lemma undefX m i ts (g : rform i ts m true) : unpack (pivot g) = undef.
proof: Proof. by case: g; case=>pivot /= /(_ (erefl _))/negbT/invalidE. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm unionmap natmap)