proposition: Lemma fndP V (f : {fmap K -> V}) k : fnd_spec f k (k \in domf f) (insub k) (f.[? k]).
proof: Proof. rewrite /fnd; case: insubP=> [[k' k'f] _ {k} <- /=|kNf]. by rewrite k'f; constructor. by rewrite (negPf kNf); constructor. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)