proposition: Lemma eq_getf V (f : {fmap K -> V}) k (kf kf' : k \in domf f) : f.[kf] = f.[kf'] :> V.
proof: Proof. by rewrite (@getfE _ _ [` kf']). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)