proposition: Lemma is_finite_for_keys (m : t A) : is_finite_forA eqb top E.eq to_function (keys_of m) m.
proof: Proof. unfold is_finite_forA, is_finite_forA', keys_of, to_function, find_default. intro k. rewrite InA_alt. setoid_rewrite in_map_iff. intro H. destruct (find k m) eqn:Hfind; simpl; [ | reflexivity ]. apply elements_iff_find in Hfind. rewrite InA_alt in Hfind. destruct Hfind as [kv [[? ?] ?]]; simpl in *; subst. exfalso; apply H. intuition eauto. Qed.
imports: Coq.FSets.FMapInterface Fiat.Common.Wf Fiat.Common.FMapExtensions Fiat.Common.FMapExtensions.LiftRelationInstances Fiat.Common