proposition: Lemma elements_correct {A} (m : t A) (i : key) (v : A) (H : find i m = Some v) : InA (eq_key_elt (elt:=A)) (i, v) (elements m).
proof: Proof. FMap_convert; assumption. Qed.
imports: Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.Program.Program Coq.Structures.OrderedTypeEx Fiat.Common Fiat.Common.SetEq Fiat.Common.SetEqProperties Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms Fiat.Common.LogicFacts Fiat.Common.SetoidClassInstances