proposition: Lemma validX m j ts1 (f1 : form (empx U) j ts1) (g: rform j ts1 m true) : valid (untag f1) -> valid (unpack (pivot g)).
proof: Proof. by case: g f1; case=>pivot H [f1][<- Sc A] /(H A); apply. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm unionmap natmap)