proposition: Lemma getf_restrict f A (k : K) (kf : k \in f) (kfA : k \in f.[& A]) : f.[& A].[kfA] = f.[kf].
proof: Proof. by rewrite get_filterf. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)