proposition: Lemma pullX' s j k ts g r (fs : form (empx U) j ts) (fg : rform j k ts g (Some r)) : untag fs = s -> unpack (pivot fg) = s \+ r.
proof: Proof. move=><-; case: fg fs; case=>pivot R [fm][E _ A1] /=. case/(_ A1 erefl): R=>S /=; rewrite -(sc_interp S A1) E. by case. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm)