proposition: Lemma fnd_if V (cond : bool) (f g : {fmap K -> V}) (k : K) : ((if cond then f else g) : finMap _ _).[? k] = if cond then f.[? k] else g.[? k].
proof: Proof. by case: cond. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)