proposition: Lemma eq_dec_comm : forall x y, (if E.eq_dec x y then true else false) = (if E.eq_dec y x then true else false).
proof: Proof. intros; destruct (E.eq_dec x y), (E.eq_dec y x); intuition. 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