proposition: Lemma expr_pf exprs1 exprs2 n (f : xfind exprs1 exprs2 n) : axiom (Context exprs1) (Context exprs2) [:: Expr n] (expr_tag (xuntag f)).
proof: Proof. case: f=>p [E H]; split=>//=; first by rewrite unitR. by rewrite andbT (onth_size E). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm)