proposition: Lemma fndSomeP f (k : K) (v : V): (f.[? k] = Some v) <-> {kf : k \in f & f.[kf] = v}.
proof: Proof. split => [fk|[kf fk]]; last by rewrite in_fnd fk. have kf : k \in f by rewrite -fndSome fk. by exists kf; apply: Some_inj; rewrite Some_fnd. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)