proposition: Lemma getf_catr f g k (kfg : k \in domf (f + g)) (kg : k \in domf g) : (f + g).[kfg] = g.[kg].
proof: Proof. by apply: Some_inj; rewrite Some_fnd fnd_cat kg in_fnd. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)