define Data.Set.Base.singleton x = (Set_sng x) define Data.Set.Base.union x y = (Set_cup x y) define Data.Set.Base.intersection x y = (Set_cap x y) define Data.Set.Base.difference x y = (Set_dif x y) define Data.Set.Base.empty = (Set_empty 0) define Data.Set.Base.null x = (Set_emp x) define Data.Set.Base.member x xs = (Set_mem x xs) define Data.Set.Base.isSubsetOf x y = (Set_sub x y) define Data.Set.Base.elems xs = (listElts xs) define GHC.Types.True = (true) define Data.Map.Base.insert k v m = (Map_store m k v) define Data.Map.Base.select k v = (Map_select m k) define Language.Haskell.Liquid.String.stringEmp = (stringEmp) define Data.RString.RString.stringEmp = (stringEmp) define String.stringEmp = (stringEmp) define Main.mempty = (mempty) define Language.Haskell.Liquid.ProofCombinators.cast x y = (y) define Control.Parallel.Strategies.withStrategy s x = (x)