proposition: Lemma onth_index (A : eqType) (s : seq A) x : onth s (index x s) = if x \in s then Some x else None.
proof: Proof. by elim: s=>//=h s IH; rewrite inE eq_sym; case: eqP=>//= ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat seq eqtype choice fintype) pcm(options axioms) Coq(Classes.Morphisms Program.Basics Program.Tactics) Coq(Relations)