proposition: Lemma eq_stronger_than_eq_key_elt : forall {A: Type} x seq, InA eq x seq -> InA (eq_key_elt (elt:=A)) x seq.
proof: Proof. intros. apply In_InA. apply equiv_eq_key_elt. induction seq; simpl in *; inversion H; subst; eauto. 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