proposition: Lemma fnd_restrict f A (k : K) : f.[& A].[? k] = if k \in A then f.[? k] else None.
proof: Proof. by rewrite fnd_filterf. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)