fact: Definition of_list (ls : list E.t) : t := List.fold_right add empty ls.
imports: Coq.MSets.MSetInterface Coq.MSets.MSetProperties Coq.MSets.MSetFacts Coq.MSets.MSetDecide Fiat.Common.Instances Fiat.Common.BoolFacts Fiat.Common