proposition: Lemma domeqX m j k rs1 rs2 ts1 (f1 : form (empx U) j ts1) (g : rform j k ts1 m (rs1, rs2)) : dom_eq (pprint k (rev rs1)) (pprint k rs2) -> dom_eq (untag f1) (unpack (pivot g)).
proof: Proof. case: g f1; case=>pivot R [f1][<- _ A1] /=; case/(_ A1): R=>S D. by rewrite !pp_interp interp_rev (sc_interp S A1). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm unionmap natmap)