proposition: Lemma recurse_pf i x xs1 xs2 (f : xfind xs1 xs2 i) : axiom (x :: xs1) (x :: xs2) i.+1 (recurse_tag (xuntag f)).
proof: Proof. by case: f=>pv [H1 H2]; split=>//; apply/prefix_cons. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq eqtype) pcm(options prelude)