proposition: Lemma oextractE (T : Type) (x : T) (xP : Some x) : oextract xP = x.
proof: Proof. by []. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)