proposition: Lemma fnd_reducef f k : (reducef f).[? k] = ojoin f.[? k].
proof: Proof. case: fndP => /= [kf|]; last by rewrite mem_reducef; case: ojoin. rewrite ffunE /= Some_oextract; apply: Some_inj; rewrite Some_fnd. by rewrite Some_ojoin // ojoinT // -mem_reducef. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)