proposition: Lemma of_ffunE key x : of_ffun key x = odflt (default x) (omap h (insub x)).
proof: Proof. rewrite /fun_of_fsfun /=. case: insubP => /= [u _ <-|xNS]; last first. case: fndP => //= kf; rewrite !ffunE /=. by set y := (X in h X); rewrite (valP y) in xNS. case: fndP => /= [kf|]. by rewrite ffunE; congr (h _); apply/val_inj => //. by rewrite inE /= -topredE /= negbK => /eqP ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)