proposition: Lemma equiv_eq_key_elt : forall {A: Type}, Equivalence (eq_key_elt (elt := A)).
proof: Proof. unfold eq_key_elt; repeat constructor; simpl in *; intuition; eauto using E.eq_trans, eq_trans. 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