proposition: Lemma recurse_pf (i : nat) (y : A) (s r : seq A) (f : xfind s r i) : invariant (y :: s) (y :: r) i.+1 f.
proof: Proof. by case:f=>[q [H1 H2]]; split; [|apply/prefix_cons]. Qed.
imports: mathcomp(ssreflect ssrnat seq) LemmaOverloading(prefix)