diff --git a/base/Control/Applicative.v b/base/Control/Applicative.v
index de457f7b..74118bb8 100644
--- a/base/Control/Applicative.v
+++ b/base/Control/Applicative.v
@@ -16,6 +16,7 @@ Require Control.Arrow.
 Require Control.Category.
 Require Data.Tuple.
 Require GHC.Base.
+Require GHC.Prim.
 Require HsToCoq.Unpeel.
 Import Control.Arrow.Notations.
 Import Control.Category.Notations.
@@ -45,31 +46,65 @@ Arguments WrapArrow {_} {_} {_} _.
 
 (* Converted value declarations: *)
 
-#[local] Definition Functor__WrappedMonad_fmap {inst_m : Type -> Type}
+(* Skipping all instances of class `GHC.Show.Show', including
+   `Control.Applicative.Show__ZipList' *)
+
+(* Skipping instance `Control.Applicative.Eq___ZipList' of class
+   `GHC.Base.Eq_' *)
+
+(* Skipping instance `Control.Applicative.Ord__ZipList' of class
+   `GHC.Base.Ord' *)
+
+(* Skipping all instances of class `GHC.Read.Read', including
+   `Control.Applicative.Read__ZipList' *)
+
+(* Skipping instance `Control.Applicative.Functor__ZipList' of class
+   `GHC.Base.Functor' *)
+
+(* Skipping instance `Control.Applicative.Foldable__ZipList' of class
+   `Data.Foldable.Foldable' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic', including
+   `Control.Applicative.Generic__ZipList' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic1', including
+   `Control.Applicative.Generic1__TYPE__ZipList__LiftedRep' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic', including
+   `Control.Applicative.Generic__WrappedArrow' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic1', including
+   `Control.Applicative.Generic1__TYPE__WrappedArrow__LiftedRep' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic', including
+   `Control.Applicative.Generic__WrappedMonad' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic1', including
+   `Control.Applicative.Generic1__TYPE__WrappedMonad__LiftedRep' *)
+
+Instance Unpeel_WrappedMonad {m} {a}
+   : HsToCoq.Unpeel.Unpeel (WrappedMonad m a) (m a) :=
+  HsToCoq.Unpeel.Build_Unpeel _ _ unwrapMonad WrapMonad.
+
+#[local] Definition Monad__WrappedMonad_op_zgzg__ {inst_m : Type -> Type}
   `{GHC.Base.Monad inst_m}
    : forall {a : Type},
-     forall {b : Type}, (a -> b) -> WrappedMonad inst_m a -> WrappedMonad inst_m b :=
-  fun {a : Type} {b : Type} =>
-    fun arg_0__ arg_1__ =>
-      match arg_0__, arg_1__ with
-      | f, WrapMonad v => WrapMonad (GHC.Base.liftM f v)
-      end.
+     forall {b : Type},
+     WrappedMonad inst_m a -> WrappedMonad inst_m b -> WrappedMonad inst_m b :=
+  fun {a : Type} {b : Type} => GHC.Prim.coerce (_GHC.Base.>>_).
 
-#[local] Definition Functor__WrappedMonad_op_zlzd__ {inst_m : Type -> Type}
+#[local] Definition Monad__WrappedMonad_op_zgzgze__ {inst_m : Type -> Type}
   `{GHC.Base.Monad inst_m}
    : forall {a : Type},
-     forall {b : Type}, a -> WrappedMonad inst_m b -> WrappedMonad inst_m a :=
-  fun {a : Type} {b : Type} =>
-    Functor__WrappedMonad_fmap GHC.Base.∘ GHC.Base.const.
+     forall {b : Type},
+     WrappedMonad inst_m a ->
+     (a -> WrappedMonad inst_m b) -> WrappedMonad inst_m b :=
+  fun {a : Type} {b : Type} => GHC.Prim.coerce (_GHC.Base.>>=_).
 
-#[global]
-Program Instance Functor__WrappedMonad {m : Type -> Type} `{GHC.Base.Monad m}
-   : GHC.Base.Functor (WrappedMonad m) :=
-  fun _ k__ =>
-    k__ {| GHC.Base.fmap__ := fun {a : Type} {b : Type} =>
-             Functor__WrappedMonad_fmap ;
-           GHC.Base.op_zlzd____ := fun {a : Type} {b : Type} =>
-             Functor__WrappedMonad_op_zlzd__ |}.
+#[local] Definition Monad__WrappedMonad_return_ {inst_m : Type -> Type}
+  `{GHC.Base.Monad inst_m}
+   : forall {a : Type}, a -> WrappedMonad inst_m a :=
+  fun {a : Type} => GHC.Prim.coerce (GHC.Base.return_).
 
 #[local] Definition Applicative__WrappedMonad_liftA2 {inst_m : Type -> Type}
   `{GHC.Base.Monad inst_m}
@@ -96,6 +131,32 @@ Program Instance Functor__WrappedMonad {m : Type -> Type} `{GHC.Base.Monad m}
       | WrapMonad f, WrapMonad v => WrapMonad (GHC.Base.ap f v)
       end.
 
+#[local] Definition Functor__WrappedMonad_fmap {inst_m : Type -> Type}
+  `{GHC.Base.Monad inst_m}
+   : forall {a : Type},
+     forall {b : Type}, (a -> b) -> WrappedMonad inst_m a -> WrappedMonad inst_m b :=
+  fun {a : Type} {b : Type} =>
+    fun arg_0__ arg_1__ =>
+      match arg_0__, arg_1__ with
+      | f, WrapMonad v => WrapMonad (GHC.Base.liftM f v)
+      end.
+
+#[local] Definition Functor__WrappedMonad_op_zlzd__ {inst_m : Type -> Type}
+  `{GHC.Base.Monad inst_m}
+   : forall {a : Type},
+     forall {b : Type}, a -> WrappedMonad inst_m b -> WrappedMonad inst_m a :=
+  fun {a : Type} {b : Type} =>
+    Functor__WrappedMonad_fmap GHC.Base.∘ GHC.Base.const.
+
+#[global]
+Program Instance Functor__WrappedMonad {m : Type -> Type} `{GHC.Base.Monad m}
+   : GHC.Base.Functor (WrappedMonad m) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.fmap__ := fun {a : Type} {b : Type} =>
+             Functor__WrappedMonad_fmap ;
+           GHC.Base.op_zlzd____ := fun {a : Type} {b : Type} =>
+             Functor__WrappedMonad_op_zlzd__ |}.
+
 #[local] Definition Applicative__WrappedMonad_op_ztzg__ {inst_m : Type -> Type}
   `{GHC.Base.Monad inst_m}
    : forall {a : Type},
@@ -123,6 +184,16 @@ Program Instance Applicative__WrappedMonad {m : Type -> Type} `{GHC.Base.Monad
              Applicative__WrappedMonad_op_ztzg__ ;
            GHC.Base.pure__ := fun {a : Type} => Applicative__WrappedMonad_pure |}.
 
+#[global]
+Program Instance Monad__WrappedMonad {m : Type -> Type} `{GHC.Base.Monad m}
+   : GHC.Base.Monad (WrappedMonad m) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zgzg____ := fun {a : Type} {b : Type} =>
+             Monad__WrappedMonad_op_zgzg__ ;
+           GHC.Base.op_zgzgze____ := fun {a : Type} {b : Type} =>
+             Monad__WrappedMonad_op_zgzgze__ ;
+           GHC.Base.return___ := fun {a : Type} => Monad__WrappedMonad_return_ |}.
+
 (* Skipping all instances of class `GHC.Base.Alternative', including
    `Control.Applicative.Alternative__WrappedMonad' *)
 
@@ -222,16 +293,14 @@ Instance Unpeel_WrappedArrow {a} {b} {c}
    : HsToCoq.Unpeel.Unpeel (WrappedArrow a b c) (a b c) :=
   HsToCoq.Unpeel.Build_Unpeel _ _ unwrapArrow WrapArrow.
 
-Instance Unpeel_WrappedMonad {m} {a}
-   : HsToCoq.Unpeel.Unpeel (WrappedMonad m a) (m a) :=
-  HsToCoq.Unpeel.Build_Unpeel _ _ unwrapMonad WrapMonad.
-
 (* External variables:
      Type Control.Arrow.Arrow Control.Arrow.arr Control.Arrow.op_zazaza__
      Control.Category.op_zgzgzg__ Data.Tuple.uncurry GHC.Base.Applicative
      GHC.Base.Functor GHC.Base.Monad GHC.Base.ap GHC.Base.const GHC.Base.fmap__
      GHC.Base.id GHC.Base.liftA2__ GHC.Base.liftM GHC.Base.liftM2
-     GHC.Base.op_z2218U__ GHC.Base.op_zlzd__ GHC.Base.op_zlzd____
-     GHC.Base.op_zlztzg____ GHC.Base.op_ztzg____ GHC.Base.pure GHC.Base.pure__
+     GHC.Base.op_z2218U__ GHC.Base.op_zgzg__ GHC.Base.op_zgzg____
+     GHC.Base.op_zgzgze__ GHC.Base.op_zgzgze____ GHC.Base.op_zlzd__
+     GHC.Base.op_zlzd____ GHC.Base.op_zlztzg____ GHC.Base.op_ztzg____ GHC.Base.pure
+     GHC.Base.pure__ GHC.Base.return_ GHC.Base.return___ GHC.Prim.coerce
      HsToCoq.Unpeel.Build_Unpeel HsToCoq.Unpeel.Unpeel
 *)
diff --git a/base/Data/Bitraversable.v b/base/Data/Bitraversable.v
index 3d3bddf2..594ed1b8 100644
--- a/base/Data/Bitraversable.v
+++ b/base/Data/Bitraversable.v
@@ -17,7 +17,7 @@ Require Data.Bifunctor.
 Require Data.Either.
 Require Data.Functor.
 Require Data.Functor.Const.
-Require Data.Functor.Identity.
+Require Import Data.Functor.Identity.
 Require Data.Functor.Utils.
 Require GHC.Base.
 Require GHC.Prim.
@@ -384,21 +384,19 @@ Program Instance Bitraversable__Const
 #[global] Definition bimapDefault {t : Type -> Type -> Type} {a : Type} {b
    : Type} {c : Type} {d : Type} `{Bitraversable t}
    : (a -> b) -> (c -> d) -> t a c -> t b d :=
-  GHC.Prim.coerce (bitraverse : (a -> Data.Functor.Identity.Identity b) ->
-                   (c -> Data.Functor.Identity.Identity d) ->
-                   t a c -> Data.Functor.Identity.Identity (t b d)).
+  GHC.Prim.coerce (bitraverse : (a -> Identity b) ->
+                   (c -> Identity d) -> t a c -> Identity (t b d)).
 
 (* Skipping definition `Data.Bitraversable.bifoldMapDefault' *)
 
 (* External variables:
-     Type op_zt__ pair Data.Bifoldable.Bifoldable Data.Bifunctor.Bifunctor
+     Identity Type op_zt__ pair Data.Bifoldable.Bifoldable Data.Bifunctor.Bifunctor
      Data.Either.Either Data.Either.Left Data.Either.Right Data.Functor.op_zlzdzg__
      Data.Functor.Const.Const Data.Functor.Const.Mk_Const
-     Data.Functor.Identity.Identity Data.Functor.Utils.Mk_StateL
-     Data.Functor.Utils.Mk_StateR Data.Functor.Utils.runStateL
-     Data.Functor.Utils.runStateR GHC.Base.Applicative GHC.Base.flip GHC.Base.id
-     GHC.Base.liftA2 GHC.Base.op_z2218U__ GHC.Prim.coerce GHC.Tuple.pair2
-     GHC.Tuple.pair3 GHC.Tuple.pair4 GHC.Tuple.pair5 GHC.Tuple.pair6 GHC.Tuple.pair7
-     GHC.Tuple.pair_type GHC.Tuple.quad_type GHC.Tuple.quint_type GHC.Tuple.sept_type
-     GHC.Tuple.sext_type GHC.Tuple.triple_type
+     Data.Functor.Utils.Mk_StateL Data.Functor.Utils.Mk_StateR
+     Data.Functor.Utils.runStateL Data.Functor.Utils.runStateR GHC.Base.Applicative
+     GHC.Base.flip GHC.Base.id GHC.Base.liftA2 GHC.Base.op_z2218U__ GHC.Prim.coerce
+     GHC.Tuple.pair2 GHC.Tuple.pair3 GHC.Tuple.pair4 GHC.Tuple.pair5 GHC.Tuple.pair6
+     GHC.Tuple.pair7 GHC.Tuple.pair_type GHC.Tuple.quad_type GHC.Tuple.quint_type
+     GHC.Tuple.sept_type GHC.Tuple.sext_type GHC.Tuple.triple_type
 *)
diff --git a/base/Data/Either.v b/base/Data/Either.v
index 6ed35ff1..d65fb873 100644
--- a/base/Data/Either.v
+++ b/base/Data/Either.v
@@ -28,6 +28,91 @@ Arguments Right {_} {_} _.
 
 (* Converted value declarations: *)
 
+#[local] Definition Eq___Either_op_zeze__ {inst_a : Type} {inst_b : Type}
+  `{GHC.Base.Eq_ inst_a} `{GHC.Base.Eq_ inst_b}
+   : Either inst_a inst_b -> Either inst_a inst_b -> bool :=
+  fun arg_0__ arg_1__ =>
+    match arg_0__, arg_1__ with
+    | Left a1, Left b1 => ((a1 GHC.Base.== b1))
+    | Right a1, Right b1 => ((a1 GHC.Base.== b1))
+    | _, _ => false
+    end.
+
+#[local] Definition Eq___Either_op_zsze__ {inst_a : Type} {inst_b : Type}
+  `{GHC.Base.Eq_ inst_a} `{GHC.Base.Eq_ inst_b}
+   : Either inst_a inst_b -> Either inst_a inst_b -> bool :=
+  fun x y => negb (Eq___Either_op_zeze__ x y).
+
+#[global]
+Program Instance Eq___Either {a : Type} {b : Type} `{GHC.Base.Eq_ a}
+  `{GHC.Base.Eq_ b}
+   : GHC.Base.Eq_ (Either a b) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zeze____ := Eq___Either_op_zeze__ ;
+           GHC.Base.op_zsze____ := Eq___Either_op_zsze__ |}.
+
+#[local] Definition Ord__Either_op_zl__ {inst_a : Type} {inst_b : Type}
+  `{GHC.Base.Ord inst_a} `{GHC.Base.Ord inst_b}
+   : Either inst_a inst_b -> Either inst_a inst_b -> bool :=
+  fun a b =>
+    match a with
+    | Left a1 => match b with | Left b1 => (a1 GHC.Base.< b1) | _ => true end
+    | Right a1 => match b with | Right b1 => (a1 GHC.Base.< b1) | _ => false end
+    end.
+
+#[local] Definition Ord__Either_op_zlze__ {inst_a : Type} {inst_b : Type}
+  `{GHC.Base.Ord inst_a} `{GHC.Base.Ord inst_b}
+   : Either inst_a inst_b -> Either inst_a inst_b -> bool :=
+  fun a b => negb (Ord__Either_op_zl__ b a).
+
+#[local] Definition Ord__Either_op_zg__ {inst_a : Type} {inst_b : Type}
+  `{GHC.Base.Ord inst_a} `{GHC.Base.Ord inst_b}
+   : Either inst_a inst_b -> Either inst_a inst_b -> bool :=
+  fun a b => Ord__Either_op_zl__ b a.
+
+#[local] Definition Ord__Either_op_zgze__ {inst_a : Type} {inst_b : Type}
+  `{GHC.Base.Ord inst_a} `{GHC.Base.Ord inst_b}
+   : Either inst_a inst_b -> Either inst_a inst_b -> bool :=
+  fun a b => negb (Ord__Either_op_zl__ a b).
+
+#[local] Definition Ord__Either_compare {inst_a : Type} {inst_b : Type}
+  `{GHC.Base.Ord inst_a} `{GHC.Base.Ord inst_b}
+   : Either inst_a inst_b -> Either inst_a inst_b -> comparison :=
+  fun a b =>
+    match a with
+    | Left a1 => match b with | Left b1 => (GHC.Base.compare a1 b1) | _ => Lt end
+    | Right a1 => match b with | Right b1 => (GHC.Base.compare a1 b1) | _ => Gt end
+    end.
+
+#[local] Definition Ord__Either_max {inst_a : Type} {inst_b : Type}
+  `{GHC.Base.Ord inst_a} `{GHC.Base.Ord inst_b}
+   : Either inst_a inst_b -> Either inst_a inst_b -> Either inst_a inst_b :=
+  fun x y => if Ord__Either_op_zlze__ x y : bool then y else x.
+
+#[local] Definition Ord__Either_min {inst_a : Type} {inst_b : Type}
+  `{GHC.Base.Ord inst_a} `{GHC.Base.Ord inst_b}
+   : Either inst_a inst_b -> Either inst_a inst_b -> Either inst_a inst_b :=
+  fun x y => if Ord__Either_op_zlze__ x y : bool then x else y.
+
+#[global]
+Program Instance Ord__Either {a : Type} {b : Type} `{GHC.Base.Ord a}
+  `{GHC.Base.Ord b}
+   : GHC.Base.Ord (Either a b) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zl____ := Ord__Either_op_zl__ ;
+           GHC.Base.op_zlze____ := Ord__Either_op_zlze__ ;
+           GHC.Base.op_zg____ := Ord__Either_op_zg__ ;
+           GHC.Base.op_zgze____ := Ord__Either_op_zgze__ ;
+           GHC.Base.compare__ := Ord__Either_compare ;
+           GHC.Base.max__ := Ord__Either_max ;
+           GHC.Base.min__ := Ord__Either_min |}.
+
+(* Skipping all instances of class `GHC.Read.Read', including
+   `Data.Either.Read__Either' *)
+
+(* Skipping all instances of class `GHC.Show.Show', including
+   `Data.Either.Show__Either' *)
+
 #[local] Definition Functor__Either_fmap {inst_a : Type}
    : forall {a : Type},
      forall {b : Type}, (a -> b) -> Either inst_a a -> Either inst_a b :=
@@ -199,11 +284,14 @@ Program Instance Monad__Either {e : Type} : GHC.Base.Monad (Either e) :=
     end.
 
 (* External variables:
-     Type bool cons false list nil op_zt__ pair true Coq.Lists.List.flat_map
-     GHC.Base.Applicative GHC.Base.Functor GHC.Base.Monad GHC.Base.Semigroup
-     GHC.Base.const GHC.Base.fmap GHC.Base.fmap__ GHC.Base.foldr GHC.Base.id
-     GHC.Base.liftA2__ GHC.Base.op_z2218U__ GHC.Base.op_zgzg____
-     GHC.Base.op_zgzgze____ GHC.Base.op_zlzd__ GHC.Base.op_zlzd____
-     GHC.Base.op_zlzlzgzg____ GHC.Base.op_zlztzg____ GHC.Base.op_ztzg____
-     GHC.Base.pure GHC.Base.pure__ GHC.Base.return___
+     Gt Lt Type bool comparison cons false list negb nil op_zt__ pair true
+     Coq.Lists.List.flat_map GHC.Base.Applicative GHC.Base.Eq_ GHC.Base.Functor
+     GHC.Base.Monad GHC.Base.Ord GHC.Base.Semigroup GHC.Base.compare
+     GHC.Base.compare__ GHC.Base.const GHC.Base.fmap GHC.Base.fmap__ GHC.Base.foldr
+     GHC.Base.id GHC.Base.liftA2__ GHC.Base.max__ GHC.Base.min__ GHC.Base.op_z2218U__
+     GHC.Base.op_zeze__ GHC.Base.op_zeze____ GHC.Base.op_zg____ GHC.Base.op_zgze____
+     GHC.Base.op_zgzg____ GHC.Base.op_zgzgze____ GHC.Base.op_zl__ GHC.Base.op_zl____
+     GHC.Base.op_zlzd__ GHC.Base.op_zlzd____ GHC.Base.op_zlze____
+     GHC.Base.op_zlzlzgzg____ GHC.Base.op_zlztzg____ GHC.Base.op_zsze____
+     GHC.Base.op_ztzg____ GHC.Base.pure GHC.Base.pure__ GHC.Base.return___
 *)
diff --git a/base/Data/Foldable.v b/base/Data/Foldable.v
index 9e25cde7..9ee470ce 100644
--- a/base/Data/Foldable.v
+++ b/base/Data/Foldable.v
@@ -21,7 +21,7 @@ Require Data.Maybe.
 Require Data.Monoid.
 Require Data.Ord.
 Require Data.Proxy.
-Require Data.SemigroupInternal.
+Require Import Data.SemigroupInternal.
 Require GHC.Base.
 Require GHC.List.
 Require GHC.Num.
@@ -132,8 +132,7 @@ Definition default_foldable {f:Type -> Type}
     (* foldMap *)
     (@foldMap)
     (* foldMap' *)
-    (fun m a (S : GHC.Base.Semigroup m) (M : GHC.Base.Monoid m) f =>
-       foldl' (fun acc a => GHC.Base.op_zlzlzgzg__ acc (f a)) GHC.Base.mempty)
+    (fun m a (S : GHC.Base.Semigroup m) (M : GHC.Base.Monoid m) f => foldl' (fun acc a => GHC.Base.op_zlzlzgzg__ acc (f a)) GHC.Base.mempty)
     (* foldl *)
     (@foldl)
     (* foldl' *)
@@ -227,10 +226,8 @@ Definition default_foldable_foldr (f : Type -> Type)
      forall {a : Type}, (b -> a -> b) -> b -> Data.Ord.Down a -> b :=
   fun {b : Type} {a : Type} =>
     fun f z t =>
-      Data.SemigroupInternal.appEndo (Data.SemigroupInternal.getDual
-                                      (Foldable__Down_foldMap (Data.SemigroupInternal.Mk_Dual GHC.Base.∘
-                                                               (Data.SemigroupInternal.Mk_Endo GHC.Base.∘
-                                                                GHC.Base.flip f)) t)) z.
+      appEndo (getDual (Foldable__Down_foldMap (Mk_Dual GHC.Base.∘
+                                                (Mk_Endo GHC.Base.∘ GHC.Base.flip f)) t)) z.
 
 #[local] Definition Foldable__Down_foldr'
    : forall {a : Type},
@@ -254,14 +251,12 @@ Definition default_foldable_foldr (f : Type -> Type)
 #[local] Definition Foldable__Down_product
    : forall {a : Type}, forall `{GHC.Num.Num a}, Data.Ord.Down a -> a :=
   fun {a : Type} `{GHC.Num.Num a} =>
-    Coq.Program.Basics.compose Data.SemigroupInternal.getProduct
-                               (Foldable__Down_foldMap Data.SemigroupInternal.Mk_Product).
+    Coq.Program.Basics.compose getProduct (Foldable__Down_foldMap Mk_Product).
 
 #[local] Definition Foldable__Down_sum
    : forall {a : Type}, forall `{GHC.Num.Num a}, Data.Ord.Down a -> a :=
   fun {a : Type} `{GHC.Num.Num a} =>
-    Coq.Program.Basics.compose Data.SemigroupInternal.getSum (Foldable__Down_foldMap
-                                Data.SemigroupInternal.Mk_Sum).
+    Coq.Program.Basics.compose getSum (Foldable__Down_foldMap Mk_Sum).
 
 #[local] Definition Foldable__Down_toList
    : forall {a : Type}, Data.Ord.Down a -> list a :=
@@ -286,620 +281,23 @@ Program Instance Foldable__Down : Foldable Data.Ord.Down :=
            sum__ := fun {a : Type} `{GHC.Num.Num a} => Foldable__Down_sum ;
            toList__ := fun {a : Type} => Foldable__Down_toList |}.
 
-#[local] Definition Foldable__UWord_foldMap
-   : forall {m : Type},
-     forall {a : Type},
-     forall `{GHC.Base.Monoid m}, (a -> m) -> GHC.Generics.UWord a -> m :=
-  fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
-    fun arg_0__ arg_1__ =>
-      match arg_0__, arg_1__ with
-      | f, GHC.Generics.UWord a1 => GHC.Base.mempty
-      end.
-
-#[local] Definition Foldable__UWord_fold
-   : forall {m : Type}, forall `{GHC.Base.Monoid m}, GHC.Generics.UWord m -> m :=
-  fun {m : Type} `{GHC.Base.Monoid m} => Foldable__UWord_foldMap GHC.Base.id.
-
-#[local] Definition Foldable__UWord_foldr
-   : forall {a : Type},
-     forall {b : Type}, (a -> b -> b) -> b -> GHC.Generics.UWord a -> b :=
-  fun {a : Type} {b : Type} =>
-    fun arg_0__ arg_1__ arg_2__ =>
-      match arg_0__, arg_1__, arg_2__ with
-      | f, z, GHC.Generics.UWord a1 => z
-      end.
-
-#[local] Definition Foldable__UWord_foldl'
-   : forall {b : Type},
-     forall {a : Type}, (b -> a -> b) -> b -> GHC.Generics.UWord a -> b :=
-  fun {b : Type} {a : Type} =>
-    fun f z0 xs =>
-      let f' := fun x k z => k (f z x) in Foldable__UWord_foldr f' GHC.Base.id xs z0.
-
-#[local] Definition Foldable__UWord_foldMap'
-   : forall {m : Type},
-     forall {a : Type},
-     forall `{GHC.Base.Monoid m}, (a -> m) -> GHC.Generics.UWord a -> m :=
-  fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
-    fun f =>
-      Foldable__UWord_foldl' (fun acc a => acc GHC.Base.<<>> f a) GHC.Base.mempty.
-
-#[local] Definition Foldable__UWord_foldl
-   : forall {b : Type},
-     forall {a : Type}, (b -> a -> b) -> b -> GHC.Generics.UWord a -> b :=
-  fun {b : Type} {a : Type} =>
-    fun f z t =>
-      Data.SemigroupInternal.appEndo (Data.SemigroupInternal.getDual
-                                      (Foldable__UWord_foldMap (Data.SemigroupInternal.Mk_Dual GHC.Base.∘
-                                                                (Data.SemigroupInternal.Mk_Endo GHC.Base.∘
-                                                                 GHC.Base.flip f)) t)) z.
-
-#[local] Definition Foldable__UWord_foldr'
-   : forall {a : Type},
-     forall {b : Type}, (a -> b -> b) -> b -> GHC.Generics.UWord a -> b :=
-  fun {a : Type} {b : Type} =>
-    fun f z0 xs =>
-      let f' := fun k x z => k (f x z) in Foldable__UWord_foldl f' GHC.Base.id xs z0.
-
-#[local] Definition Foldable__UWord_length
-   : forall {a : Type}, GHC.Generics.UWord a -> GHC.Num.Int :=
-  fun {a : Type} =>
-    Foldable__UWord_foldl' (fun arg_0__ arg_1__ =>
-                              match arg_0__, arg_1__ with
-                              | c, _ => c GHC.Num.+ #1
-                              end) #0.
-
-#[local] Definition Foldable__UWord_null
-   : forall {a : Type}, GHC.Generics.UWord a -> bool :=
-  fun {a : Type} => fun '(GHC.Generics.UWord a1) => true.
-
-#[local] Definition Foldable__UWord_product
-   : forall {a : Type}, forall `{GHC.Num.Num a}, GHC.Generics.UWord a -> a :=
-  fun {a : Type} `{GHC.Num.Num a} =>
-    Coq.Program.Basics.compose Data.SemigroupInternal.getProduct
-                               (Foldable__UWord_foldMap Data.SemigroupInternal.Mk_Product).
-
-#[local] Definition Foldable__UWord_sum
-   : forall {a : Type}, forall `{GHC.Num.Num a}, GHC.Generics.UWord a -> a :=
-  fun {a : Type} `{GHC.Num.Num a} =>
-    Coq.Program.Basics.compose Data.SemigroupInternal.getSum
-                               (Foldable__UWord_foldMap Data.SemigroupInternal.Mk_Sum).
-
-#[local] Definition Foldable__UWord_toList
-   : forall {a : Type}, GHC.Generics.UWord a -> list a :=
-  fun {a : Type} =>
-    fun t => GHC.Base.build' (fun _ => (fun c n => Foldable__UWord_foldr c n t)).
-
-#[global]
-Program Instance Foldable__UWord : Foldable GHC.Generics.UWord :=
-  fun _ k__ =>
-    k__ {| fold__ := fun {m : Type} `{GHC.Base.Monoid m} => Foldable__UWord_fold ;
-           foldMap__ := fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
-             Foldable__UWord_foldMap ;
-           foldMap'__ := fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
-             Foldable__UWord_foldMap' ;
-           foldl__ := fun {b : Type} {a : Type} => Foldable__UWord_foldl ;
-           foldl'__ := fun {b : Type} {a : Type} => Foldable__UWord_foldl' ;
-           foldr__ := fun {a : Type} {b : Type} => Foldable__UWord_foldr ;
-           foldr'__ := fun {a : Type} {b : Type} => Foldable__UWord_foldr' ;
-           length__ := fun {a : Type} => Foldable__UWord_length ;
-           null__ := fun {a : Type} => Foldable__UWord_null ;
-           product__ := fun {a : Type} `{GHC.Num.Num a} => Foldable__UWord_product ;
-           sum__ := fun {a : Type} `{GHC.Num.Num a} => Foldable__UWord_sum ;
-           toList__ := fun {a : Type} => Foldable__UWord_toList |}.
-
-#[local] Definition Foldable__UInt_foldMap
-   : forall {m : Type},
-     forall {a : Type},
-     forall `{GHC.Base.Monoid m}, (a -> m) -> GHC.Generics.UInt a -> m :=
-  fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
-    fun arg_0__ arg_1__ =>
-      match arg_0__, arg_1__ with
-      | f, GHC.Generics.UInt a1 => GHC.Base.mempty
-      end.
-
-#[local] Definition Foldable__UInt_fold
-   : forall {m : Type}, forall `{GHC.Base.Monoid m}, GHC.Generics.UInt m -> m :=
-  fun {m : Type} `{GHC.Base.Monoid m} => Foldable__UInt_foldMap GHC.Base.id.
-
-#[local] Definition Foldable__UInt_foldr
-   : forall {a : Type},
-     forall {b : Type}, (a -> b -> b) -> b -> GHC.Generics.UInt a -> b :=
-  fun {a : Type} {b : Type} =>
-    fun arg_0__ arg_1__ arg_2__ =>
-      match arg_0__, arg_1__, arg_2__ with
-      | f, z, GHC.Generics.UInt a1 => z
-      end.
-
-#[local] Definition Foldable__UInt_foldl'
-   : forall {b : Type},
-     forall {a : Type}, (b -> a -> b) -> b -> GHC.Generics.UInt a -> b :=
-  fun {b : Type} {a : Type} =>
-    fun f z0 xs =>
-      let f' := fun x k z => k (f z x) in Foldable__UInt_foldr f' GHC.Base.id xs z0.
-
-#[local] Definition Foldable__UInt_foldMap'
-   : forall {m : Type},
-     forall {a : Type},
-     forall `{GHC.Base.Monoid m}, (a -> m) -> GHC.Generics.UInt a -> m :=
-  fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
-    fun f =>
-      Foldable__UInt_foldl' (fun acc a => acc GHC.Base.<<>> f a) GHC.Base.mempty.
-
-#[local] Definition Foldable__UInt_foldl
-   : forall {b : Type},
-     forall {a : Type}, (b -> a -> b) -> b -> GHC.Generics.UInt a -> b :=
-  fun {b : Type} {a : Type} =>
-    fun f z t =>
-      Data.SemigroupInternal.appEndo (Data.SemigroupInternal.getDual
-                                      (Foldable__UInt_foldMap (Data.SemigroupInternal.Mk_Dual GHC.Base.∘
-                                                               (Data.SemigroupInternal.Mk_Endo GHC.Base.∘
-                                                                GHC.Base.flip f)) t)) z.
-
-#[local] Definition Foldable__UInt_foldr'
-   : forall {a : Type},
-     forall {b : Type}, (a -> b -> b) -> b -> GHC.Generics.UInt a -> b :=
-  fun {a : Type} {b : Type} =>
-    fun f z0 xs =>
-      let f' := fun k x z => k (f x z) in Foldable__UInt_foldl f' GHC.Base.id xs z0.
-
-#[local] Definition Foldable__UInt_length
-   : forall {a : Type}, GHC.Generics.UInt a -> GHC.Num.Int :=
-  fun {a : Type} =>
-    Foldable__UInt_foldl' (fun arg_0__ arg_1__ =>
-                             match arg_0__, arg_1__ with
-                             | c, _ => c GHC.Num.+ #1
-                             end) #0.
-
-#[local] Definition Foldable__UInt_null
-   : forall {a : Type}, GHC.Generics.UInt a -> bool :=
-  fun {a : Type} => fun '(GHC.Generics.UInt a1) => true.
-
-#[local] Definition Foldable__UInt_product
-   : forall {a : Type}, forall `{GHC.Num.Num a}, GHC.Generics.UInt a -> a :=
-  fun {a : Type} `{GHC.Num.Num a} =>
-    Coq.Program.Basics.compose Data.SemigroupInternal.getProduct
-                               (Foldable__UInt_foldMap Data.SemigroupInternal.Mk_Product).
-
-#[local] Definition Foldable__UInt_sum
-   : forall {a : Type}, forall `{GHC.Num.Num a}, GHC.Generics.UInt a -> a :=
-  fun {a : Type} `{GHC.Num.Num a} =>
-    Coq.Program.Basics.compose Data.SemigroupInternal.getSum (Foldable__UInt_foldMap
-                                Data.SemigroupInternal.Mk_Sum).
-
-#[local] Definition Foldable__UInt_toList
-   : forall {a : Type}, GHC.Generics.UInt a -> list a :=
-  fun {a : Type} =>
-    fun t => GHC.Base.build' (fun _ => (fun c n => Foldable__UInt_foldr c n t)).
-
-#[global]
-Program Instance Foldable__UInt : Foldable GHC.Generics.UInt :=
-  fun _ k__ =>
-    k__ {| fold__ := fun {m : Type} `{GHC.Base.Monoid m} => Foldable__UInt_fold ;
-           foldMap__ := fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
-             Foldable__UInt_foldMap ;
-           foldMap'__ := fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
-             Foldable__UInt_foldMap' ;
-           foldl__ := fun {b : Type} {a : Type} => Foldable__UInt_foldl ;
-           foldl'__ := fun {b : Type} {a : Type} => Foldable__UInt_foldl' ;
-           foldr__ := fun {a : Type} {b : Type} => Foldable__UInt_foldr ;
-           foldr'__ := fun {a : Type} {b : Type} => Foldable__UInt_foldr' ;
-           length__ := fun {a : Type} => Foldable__UInt_length ;
-           null__ := fun {a : Type} => Foldable__UInt_null ;
-           product__ := fun {a : Type} `{GHC.Num.Num a} => Foldable__UInt_product ;
-           sum__ := fun {a : Type} `{GHC.Num.Num a} => Foldable__UInt_sum ;
-           toList__ := fun {a : Type} => Foldable__UInt_toList |}.
-
-#[local] Definition Foldable__UFloat_foldMap
-   : forall {m : Type},
-     forall {a : Type},
-     forall `{GHC.Base.Monoid m}, (a -> m) -> GHC.Generics.UFloat a -> m :=
-  fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
-    fun arg_0__ arg_1__ =>
-      match arg_0__, arg_1__ with
-      | f, GHC.Generics.UFloat a1 => GHC.Base.mempty
-      end.
-
-#[local] Definition Foldable__UFloat_fold
-   : forall {m : Type}, forall `{GHC.Base.Monoid m}, GHC.Generics.UFloat m -> m :=
-  fun {m : Type} `{GHC.Base.Monoid m} => Foldable__UFloat_foldMap GHC.Base.id.
-
-#[local] Definition Foldable__UFloat_foldr
-   : forall {a : Type},
-     forall {b : Type}, (a -> b -> b) -> b -> GHC.Generics.UFloat a -> b :=
-  fun {a : Type} {b : Type} =>
-    fun arg_0__ arg_1__ arg_2__ =>
-      match arg_0__, arg_1__, arg_2__ with
-      | f, z, GHC.Generics.UFloat a1 => z
-      end.
-
-#[local] Definition Foldable__UFloat_foldl'
-   : forall {b : Type},
-     forall {a : Type}, (b -> a -> b) -> b -> GHC.Generics.UFloat a -> b :=
-  fun {b : Type} {a : Type} =>
-    fun f z0 xs =>
-      let f' := fun x k z => k (f z x) in Foldable__UFloat_foldr f' GHC.Base.id xs z0.
-
-#[local] Definition Foldable__UFloat_foldMap'
-   : forall {m : Type},
-     forall {a : Type},
-     forall `{GHC.Base.Monoid m}, (a -> m) -> GHC.Generics.UFloat a -> m :=
-  fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
-    fun f =>
-      Foldable__UFloat_foldl' (fun acc a => acc GHC.Base.<<>> f a) GHC.Base.mempty.
-
-#[local] Definition Foldable__UFloat_foldl
-   : forall {b : Type},
-     forall {a : Type}, (b -> a -> b) -> b -> GHC.Generics.UFloat a -> b :=
-  fun {b : Type} {a : Type} =>
-    fun f z t =>
-      Data.SemigroupInternal.appEndo (Data.SemigroupInternal.getDual
-                                      (Foldable__UFloat_foldMap (Data.SemigroupInternal.Mk_Dual GHC.Base.∘
-                                                                 (Data.SemigroupInternal.Mk_Endo GHC.Base.∘
-                                                                  GHC.Base.flip f)) t)) z.
-
-#[local] Definition Foldable__UFloat_foldr'
-   : forall {a : Type},
-     forall {b : Type}, (a -> b -> b) -> b -> GHC.Generics.UFloat a -> b :=
-  fun {a : Type} {b : Type} =>
-    fun f z0 xs =>
-      let f' := fun k x z => k (f x z) in Foldable__UFloat_foldl f' GHC.Base.id xs z0.
-
-#[local] Definition Foldable__UFloat_length
-   : forall {a : Type}, GHC.Generics.UFloat a -> GHC.Num.Int :=
-  fun {a : Type} =>
-    Foldable__UFloat_foldl' (fun arg_0__ arg_1__ =>
-                               match arg_0__, arg_1__ with
-                               | c, _ => c GHC.Num.+ #1
-                               end) #0.
-
-#[local] Definition Foldable__UFloat_null
-   : forall {a : Type}, GHC.Generics.UFloat a -> bool :=
-  fun {a : Type} => fun '(GHC.Generics.UFloat a1) => true.
-
-#[local] Definition Foldable__UFloat_product
-   : forall {a : Type}, forall `{GHC.Num.Num a}, GHC.Generics.UFloat a -> a :=
-  fun {a : Type} `{GHC.Num.Num a} =>
-    Coq.Program.Basics.compose Data.SemigroupInternal.getProduct
-                               (Foldable__UFloat_foldMap Data.SemigroupInternal.Mk_Product).
-
-#[local] Definition Foldable__UFloat_sum
-   : forall {a : Type}, forall `{GHC.Num.Num a}, GHC.Generics.UFloat a -> a :=
-  fun {a : Type} `{GHC.Num.Num a} =>
-    Coq.Program.Basics.compose Data.SemigroupInternal.getSum
-                               (Foldable__UFloat_foldMap Data.SemigroupInternal.Mk_Sum).
-
-#[local] Definition Foldable__UFloat_toList
-   : forall {a : Type}, GHC.Generics.UFloat a -> list a :=
-  fun {a : Type} =>
-    fun t => GHC.Base.build' (fun _ => (fun c n => Foldable__UFloat_foldr c n t)).
-
-#[global]
-Program Instance Foldable__UFloat : Foldable GHC.Generics.UFloat :=
-  fun _ k__ =>
-    k__ {| fold__ := fun {m : Type} `{GHC.Base.Monoid m} => Foldable__UFloat_fold ;
-           foldMap__ := fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
-             Foldable__UFloat_foldMap ;
-           foldMap'__ := fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
-             Foldable__UFloat_foldMap' ;
-           foldl__ := fun {b : Type} {a : Type} => Foldable__UFloat_foldl ;
-           foldl'__ := fun {b : Type} {a : Type} => Foldable__UFloat_foldl' ;
-           foldr__ := fun {a : Type} {b : Type} => Foldable__UFloat_foldr ;
-           foldr'__ := fun {a : Type} {b : Type} => Foldable__UFloat_foldr' ;
-           length__ := fun {a : Type} => Foldable__UFloat_length ;
-           null__ := fun {a : Type} => Foldable__UFloat_null ;
-           product__ := fun {a : Type} `{GHC.Num.Num a} => Foldable__UFloat_product ;
-           sum__ := fun {a : Type} `{GHC.Num.Num a} => Foldable__UFloat_sum ;
-           toList__ := fun {a : Type} => Foldable__UFloat_toList |}.
-
-#[local] Definition Foldable__UDouble_foldMap
-   : forall {m : Type},
-     forall {a : Type},
-     forall `{GHC.Base.Monoid m}, (a -> m) -> GHC.Generics.UDouble a -> m :=
-  fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
-    fun arg_0__ arg_1__ =>
-      match arg_0__, arg_1__ with
-      | f, GHC.Generics.UDouble a1 => GHC.Base.mempty
-      end.
-
-#[local] Definition Foldable__UDouble_fold
-   : forall {m : Type},
-     forall `{GHC.Base.Monoid m}, GHC.Generics.UDouble m -> m :=
-  fun {m : Type} `{GHC.Base.Monoid m} => Foldable__UDouble_foldMap GHC.Base.id.
-
-#[local] Definition Foldable__UDouble_foldr
-   : forall {a : Type},
-     forall {b : Type}, (a -> b -> b) -> b -> GHC.Generics.UDouble a -> b :=
-  fun {a : Type} {b : Type} =>
-    fun arg_0__ arg_1__ arg_2__ =>
-      match arg_0__, arg_1__, arg_2__ with
-      | f, z, GHC.Generics.UDouble a1 => z
-      end.
-
-#[local] Definition Foldable__UDouble_foldl'
-   : forall {b : Type},
-     forall {a : Type}, (b -> a -> b) -> b -> GHC.Generics.UDouble a -> b :=
-  fun {b : Type} {a : Type} =>
-    fun f z0 xs =>
-      let f' := fun x k z => k (f z x) in
-      Foldable__UDouble_foldr f' GHC.Base.id xs z0.
-
-#[local] Definition Foldable__UDouble_foldMap'
-   : forall {m : Type},
-     forall {a : Type},
-     forall `{GHC.Base.Monoid m}, (a -> m) -> GHC.Generics.UDouble a -> m :=
-  fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
-    fun f =>
-      Foldable__UDouble_foldl' (fun acc a => acc GHC.Base.<<>> f a) GHC.Base.mempty.
-
-#[local] Definition Foldable__UDouble_foldl
-   : forall {b : Type},
-     forall {a : Type}, (b -> a -> b) -> b -> GHC.Generics.UDouble a -> b :=
-  fun {b : Type} {a : Type} =>
-    fun f z t =>
-      Data.SemigroupInternal.appEndo (Data.SemigroupInternal.getDual
-                                      (Foldable__UDouble_foldMap (Data.SemigroupInternal.Mk_Dual GHC.Base.∘
-                                                                  (Data.SemigroupInternal.Mk_Endo GHC.Base.∘
-                                                                   GHC.Base.flip f)) t)) z.
-
-#[local] Definition Foldable__UDouble_foldr'
-   : forall {a : Type},
-     forall {b : Type}, (a -> b -> b) -> b -> GHC.Generics.UDouble a -> b :=
-  fun {a : Type} {b : Type} =>
-    fun f z0 xs =>
-      let f' := fun k x z => k (f x z) in
-      Foldable__UDouble_foldl f' GHC.Base.id xs z0.
-
-#[local] Definition Foldable__UDouble_length
-   : forall {a : Type}, GHC.Generics.UDouble a -> GHC.Num.Int :=
-  fun {a : Type} =>
-    Foldable__UDouble_foldl' (fun arg_0__ arg_1__ =>
-                                match arg_0__, arg_1__ with
-                                | c, _ => c GHC.Num.+ #1
-                                end) #0.
-
-#[local] Definition Foldable__UDouble_null
-   : forall {a : Type}, GHC.Generics.UDouble a -> bool :=
-  fun {a : Type} => fun '(GHC.Generics.UDouble a1) => true.
-
-#[local] Definition Foldable__UDouble_product
-   : forall {a : Type}, forall `{GHC.Num.Num a}, GHC.Generics.UDouble a -> a :=
-  fun {a : Type} `{GHC.Num.Num a} =>
-    Coq.Program.Basics.compose Data.SemigroupInternal.getProduct
-                               (Foldable__UDouble_foldMap Data.SemigroupInternal.Mk_Product).
-
-#[local] Definition Foldable__UDouble_sum
-   : forall {a : Type}, forall `{GHC.Num.Num a}, GHC.Generics.UDouble a -> a :=
-  fun {a : Type} `{GHC.Num.Num a} =>
-    Coq.Program.Basics.compose Data.SemigroupInternal.getSum
-                               (Foldable__UDouble_foldMap Data.SemigroupInternal.Mk_Sum).
-
-#[local] Definition Foldable__UDouble_toList
-   : forall {a : Type}, GHC.Generics.UDouble a -> list a :=
-  fun {a : Type} =>
-    fun t => GHC.Base.build' (fun _ => (fun c n => Foldable__UDouble_foldr c n t)).
-
-#[global]
-Program Instance Foldable__UDouble : Foldable GHC.Generics.UDouble :=
-  fun _ k__ =>
-    k__ {| fold__ := fun {m : Type} `{GHC.Base.Monoid m} => Foldable__UDouble_fold ;
-           foldMap__ := fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
-             Foldable__UDouble_foldMap ;
-           foldMap'__ := fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
-             Foldable__UDouble_foldMap' ;
-           foldl__ := fun {b : Type} {a : Type} => Foldable__UDouble_foldl ;
-           foldl'__ := fun {b : Type} {a : Type} => Foldable__UDouble_foldl' ;
-           foldr__ := fun {a : Type} {b : Type} => Foldable__UDouble_foldr ;
-           foldr'__ := fun {a : Type} {b : Type} => Foldable__UDouble_foldr' ;
-           length__ := fun {a : Type} => Foldable__UDouble_length ;
-           null__ := fun {a : Type} => Foldable__UDouble_null ;
-           product__ := fun {a : Type} `{GHC.Num.Num a} => Foldable__UDouble_product ;
-           sum__ := fun {a : Type} `{GHC.Num.Num a} => Foldable__UDouble_sum ;
-           toList__ := fun {a : Type} => Foldable__UDouble_toList |}.
-
-#[local] Definition Foldable__UChar_foldMap
-   : forall {m : Type},
-     forall {a : Type},
-     forall `{GHC.Base.Monoid m}, (a -> m) -> GHC.Generics.UChar a -> m :=
-  fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
-    fun arg_0__ arg_1__ =>
-      match arg_0__, arg_1__ with
-      | f, GHC.Generics.UChar a1 => GHC.Base.mempty
-      end.
-
-#[local] Definition Foldable__UChar_fold
-   : forall {m : Type}, forall `{GHC.Base.Monoid m}, GHC.Generics.UChar m -> m :=
-  fun {m : Type} `{GHC.Base.Monoid m} => Foldable__UChar_foldMap GHC.Base.id.
-
-#[local] Definition Foldable__UChar_foldr
-   : forall {a : Type},
-     forall {b : Type}, (a -> b -> b) -> b -> GHC.Generics.UChar a -> b :=
-  fun {a : Type} {b : Type} =>
-    fun arg_0__ arg_1__ arg_2__ =>
-      match arg_0__, arg_1__, arg_2__ with
-      | f, z, GHC.Generics.UChar a1 => z
-      end.
-
-#[local] Definition Foldable__UChar_foldl'
-   : forall {b : Type},
-     forall {a : Type}, (b -> a -> b) -> b -> GHC.Generics.UChar a -> b :=
-  fun {b : Type} {a : Type} =>
-    fun f z0 xs =>
-      let f' := fun x k z => k (f z x) in Foldable__UChar_foldr f' GHC.Base.id xs z0.
-
-#[local] Definition Foldable__UChar_foldMap'
-   : forall {m : Type},
-     forall {a : Type},
-     forall `{GHC.Base.Monoid m}, (a -> m) -> GHC.Generics.UChar a -> m :=
-  fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
-    fun f =>
-      Foldable__UChar_foldl' (fun acc a => acc GHC.Base.<<>> f a) GHC.Base.mempty.
-
-#[local] Definition Foldable__UChar_foldl
-   : forall {b : Type},
-     forall {a : Type}, (b -> a -> b) -> b -> GHC.Generics.UChar a -> b :=
-  fun {b : Type} {a : Type} =>
-    fun f z t =>
-      Data.SemigroupInternal.appEndo (Data.SemigroupInternal.getDual
-                                      (Foldable__UChar_foldMap (Data.SemigroupInternal.Mk_Dual GHC.Base.∘
-                                                                (Data.SemigroupInternal.Mk_Endo GHC.Base.∘
-                                                                 GHC.Base.flip f)) t)) z.
-
-#[local] Definition Foldable__UChar_foldr'
-   : forall {a : Type},
-     forall {b : Type}, (a -> b -> b) -> b -> GHC.Generics.UChar a -> b :=
-  fun {a : Type} {b : Type} =>
-    fun f z0 xs =>
-      let f' := fun k x z => k (f x z) in Foldable__UChar_foldl f' GHC.Base.id xs z0.
-
-#[local] Definition Foldable__UChar_length
-   : forall {a : Type}, GHC.Generics.UChar a -> GHC.Num.Int :=
-  fun {a : Type} =>
-    Foldable__UChar_foldl' (fun arg_0__ arg_1__ =>
-                              match arg_0__, arg_1__ with
-                              | c, _ => c GHC.Num.+ #1
-                              end) #0.
-
-#[local] Definition Foldable__UChar_null
-   : forall {a : Type}, GHC.Generics.UChar a -> bool :=
-  fun {a : Type} => fun '(GHC.Generics.UChar a1) => true.
-
-#[local] Definition Foldable__UChar_product
-   : forall {a : Type}, forall `{GHC.Num.Num a}, GHC.Generics.UChar a -> a :=
-  fun {a : Type} `{GHC.Num.Num a} =>
-    Coq.Program.Basics.compose Data.SemigroupInternal.getProduct
-                               (Foldable__UChar_foldMap Data.SemigroupInternal.Mk_Product).
-
-#[local] Definition Foldable__UChar_sum
-   : forall {a : Type}, forall `{GHC.Num.Num a}, GHC.Generics.UChar a -> a :=
-  fun {a : Type} `{GHC.Num.Num a} =>
-    Coq.Program.Basics.compose Data.SemigroupInternal.getSum
-                               (Foldable__UChar_foldMap Data.SemigroupInternal.Mk_Sum).
-
-#[local] Definition Foldable__UChar_toList
-   : forall {a : Type}, GHC.Generics.UChar a -> list a :=
-  fun {a : Type} =>
-    fun t => GHC.Base.build' (fun _ => (fun c n => Foldable__UChar_foldr c n t)).
-
-#[global]
-Program Instance Foldable__UChar : Foldable GHC.Generics.UChar :=
-  fun _ k__ =>
-    k__ {| fold__ := fun {m : Type} `{GHC.Base.Monoid m} => Foldable__UChar_fold ;
-           foldMap__ := fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
-             Foldable__UChar_foldMap ;
-           foldMap'__ := fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
-             Foldable__UChar_foldMap' ;
-           foldl__ := fun {b : Type} {a : Type} => Foldable__UChar_foldl ;
-           foldl'__ := fun {b : Type} {a : Type} => Foldable__UChar_foldl' ;
-           foldr__ := fun {a : Type} {b : Type} => Foldable__UChar_foldr ;
-           foldr'__ := fun {a : Type} {b : Type} => Foldable__UChar_foldr' ;
-           length__ := fun {a : Type} => Foldable__UChar_length ;
-           null__ := fun {a : Type} => Foldable__UChar_null ;
-           product__ := fun {a : Type} `{GHC.Num.Num a} => Foldable__UChar_product ;
-           sum__ := fun {a : Type} `{GHC.Num.Num a} => Foldable__UChar_sum ;
-           toList__ := fun {a : Type} => Foldable__UChar_toList |}.
-
-#[local] Definition Foldable__UAddr_foldMap
-   : forall {m : Type},
-     forall {a : Type},
-     forall `{GHC.Base.Monoid m}, (a -> m) -> GHC.Generics.UAddr a -> m :=
-  fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
-    fun arg_0__ arg_1__ =>
-      match arg_0__, arg_1__ with
-      | f, GHC.Generics.UAddr a1 => GHC.Base.mempty
-      end.
-
-#[local] Definition Foldable__UAddr_fold
-   : forall {m : Type}, forall `{GHC.Base.Monoid m}, GHC.Generics.UAddr m -> m :=
-  fun {m : Type} `{GHC.Base.Monoid m} => Foldable__UAddr_foldMap GHC.Base.id.
-
-#[local] Definition Foldable__UAddr_foldr
-   : forall {a : Type},
-     forall {b : Type}, (a -> b -> b) -> b -> GHC.Generics.UAddr a -> b :=
-  fun {a : Type} {b : Type} =>
-    fun arg_0__ arg_1__ arg_2__ =>
-      match arg_0__, arg_1__, arg_2__ with
-      | f, z, GHC.Generics.UAddr a1 => z
-      end.
-
-#[local] Definition Foldable__UAddr_foldl'
-   : forall {b : Type},
-     forall {a : Type}, (b -> a -> b) -> b -> GHC.Generics.UAddr a -> b :=
-  fun {b : Type} {a : Type} =>
-    fun f z0 xs =>
-      let f' := fun x k z => k (f z x) in Foldable__UAddr_foldr f' GHC.Base.id xs z0.
-
-#[local] Definition Foldable__UAddr_foldMap'
-   : forall {m : Type},
-     forall {a : Type},
-     forall `{GHC.Base.Monoid m}, (a -> m) -> GHC.Generics.UAddr a -> m :=
-  fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
-    fun f =>
-      Foldable__UAddr_foldl' (fun acc a => acc GHC.Base.<<>> f a) GHC.Base.mempty.
-
-#[local] Definition Foldable__UAddr_foldl
-   : forall {b : Type},
-     forall {a : Type}, (b -> a -> b) -> b -> GHC.Generics.UAddr a -> b :=
-  fun {b : Type} {a : Type} =>
-    fun f z t =>
-      Data.SemigroupInternal.appEndo (Data.SemigroupInternal.getDual
-                                      (Foldable__UAddr_foldMap (Data.SemigroupInternal.Mk_Dual GHC.Base.∘
-                                                                (Data.SemigroupInternal.Mk_Endo GHC.Base.∘
-                                                                 GHC.Base.flip f)) t)) z.
-
-#[local] Definition Foldable__UAddr_foldr'
-   : forall {a : Type},
-     forall {b : Type}, (a -> b -> b) -> b -> GHC.Generics.UAddr a -> b :=
-  fun {a : Type} {b : Type} =>
-    fun f z0 xs =>
-      let f' := fun k x z => k (f x z) in Foldable__UAddr_foldl f' GHC.Base.id xs z0.
-
-#[local] Definition Foldable__UAddr_length
-   : forall {a : Type}, GHC.Generics.UAddr a -> GHC.Num.Int :=
-  fun {a : Type} =>
-    Foldable__UAddr_foldl' (fun arg_0__ arg_1__ =>
-                              match arg_0__, arg_1__ with
-                              | c, _ => c GHC.Num.+ #1
-                              end) #0.
+(* Skipping instance `Data.Foldable.Foldable__UWord' of class
+   `Data.Foldable.Foldable' *)
 
-#[local] Definition Foldable__UAddr_null
-   : forall {a : Type}, GHC.Generics.UAddr a -> bool :=
-  fun {a : Type} => fun '(GHC.Generics.UAddr a1) => true.
+(* Skipping instance `Data.Foldable.Foldable__UInt' of class
+   `Data.Foldable.Foldable' *)
 
-#[local] Definition Foldable__UAddr_product
-   : forall {a : Type}, forall `{GHC.Num.Num a}, GHC.Generics.UAddr a -> a :=
-  fun {a : Type} `{GHC.Num.Num a} =>
-    Coq.Program.Basics.compose Data.SemigroupInternal.getProduct
-                               (Foldable__UAddr_foldMap Data.SemigroupInternal.Mk_Product).
+(* Skipping instance `Data.Foldable.Foldable__UFloat' of class
+   `Data.Foldable.Foldable' *)
 
-#[local] Definition Foldable__UAddr_sum
-   : forall {a : Type}, forall `{GHC.Num.Num a}, GHC.Generics.UAddr a -> a :=
-  fun {a : Type} `{GHC.Num.Num a} =>
-    Coq.Program.Basics.compose Data.SemigroupInternal.getSum
-                               (Foldable__UAddr_foldMap Data.SemigroupInternal.Mk_Sum).
+(* Skipping instance `Data.Foldable.Foldable__UDouble' of class
+   `Data.Foldable.Foldable' *)
 
-#[local] Definition Foldable__UAddr_toList
-   : forall {a : Type}, GHC.Generics.UAddr a -> list a :=
-  fun {a : Type} =>
-    fun t => GHC.Base.build' (fun _ => (fun c n => Foldable__UAddr_foldr c n t)).
+(* Skipping instance `Data.Foldable.Foldable__UChar' of class
+   `Data.Foldable.Foldable' *)
 
-#[global]
-Program Instance Foldable__UAddr : Foldable GHC.Generics.UAddr :=
-  fun _ k__ =>
-    k__ {| fold__ := fun {m : Type} `{GHC.Base.Monoid m} => Foldable__UAddr_fold ;
-           foldMap__ := fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
-             Foldable__UAddr_foldMap ;
-           foldMap'__ := fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
-             Foldable__UAddr_foldMap' ;
-           foldl__ := fun {b : Type} {a : Type} => Foldable__UAddr_foldl ;
-           foldl'__ := fun {b : Type} {a : Type} => Foldable__UAddr_foldl' ;
-           foldr__ := fun {a : Type} {b : Type} => Foldable__UAddr_foldr ;
-           foldr'__ := fun {a : Type} {b : Type} => Foldable__UAddr_foldr' ;
-           length__ := fun {a : Type} => Foldable__UAddr_length ;
-           null__ := fun {a : Type} => Foldable__UAddr_null ;
-           product__ := fun {a : Type} `{GHC.Num.Num a} => Foldable__UAddr_product ;
-           sum__ := fun {a : Type} `{GHC.Num.Num a} => Foldable__UAddr_sum ;
-           toList__ := fun {a : Type} => Foldable__UAddr_toList |}.
+(* Skipping instance `Data.Foldable.Foldable__UAddr' of class
+   `Data.Foldable.Foldable' *)
 
 (* Skipping instance `Data.Foldable.Foldable__op_ZCziZC__' of class
    `Data.Foldable.Foldable' *)
@@ -987,14 +385,12 @@ Program Instance Foldable__UAddr : Foldable GHC.Generics.UAddr :=
 #[local] Definition Foldable__option_product
    : forall {a : Type}, forall `{GHC.Num.Num a}, option a -> a :=
   fun {a : Type} `{GHC.Num.Num a} =>
-    Coq.Program.Basics.compose Data.SemigroupInternal.getProduct
-                               (Foldable__option_foldMap Data.SemigroupInternal.Mk_Product).
+    Coq.Program.Basics.compose getProduct (Foldable__option_foldMap Mk_Product).
 
 #[local] Definition Foldable__option_sum
    : forall {a : Type}, forall `{GHC.Num.Num a}, option a -> a :=
   fun {a : Type} `{GHC.Num.Num a} =>
-    Coq.Program.Basics.compose Data.SemigroupInternal.getSum
-                               (Foldable__option_foldMap Data.SemigroupInternal.Mk_Sum).
+    Coq.Program.Basics.compose getSum (Foldable__option_foldMap Mk_Sum).
 
 #[local] Definition Foldable__option_toList
    : forall {a : Type}, option a -> list a :=
@@ -1163,14 +559,12 @@ Program Instance Foldable__list : Foldable list :=
 #[local] Definition Foldable__NonEmpty_product
    : forall {a : Type}, forall `{GHC.Num.Num a}, GHC.Base.NonEmpty a -> a :=
   fun {a : Type} `{GHC.Num.Num a} =>
-    Coq.Program.Basics.compose Data.SemigroupInternal.getProduct
-                               (Foldable__NonEmpty_foldMap Data.SemigroupInternal.Mk_Product).
+    Coq.Program.Basics.compose getProduct (Foldable__NonEmpty_foldMap Mk_Product).
 
 #[local] Definition Foldable__NonEmpty_sum
    : forall {a : Type}, forall `{GHC.Num.Num a}, GHC.Base.NonEmpty a -> a :=
   fun {a : Type} `{GHC.Num.Num a} =>
-    Coq.Program.Basics.compose Data.SemigroupInternal.getSum
-                               (Foldable__NonEmpty_foldMap Data.SemigroupInternal.Mk_Sum).
+    Coq.Program.Basics.compose getSum (Foldable__NonEmpty_foldMap Mk_Sum).
 
 #[local] Definition Foldable__NonEmpty_toList
    : forall {a : Type}, GHC.Base.NonEmpty a -> list a :=
@@ -1241,10 +635,8 @@ Program Instance Foldable__NonEmpty : Foldable GHC.Base.NonEmpty :=
      forall {a : Type}, (b -> a -> b) -> b -> Data.Either.Either inst_a a -> b :=
   fun {b : Type} {a : Type} =>
     fun f z t =>
-      Data.SemigroupInternal.appEndo (Data.SemigroupInternal.getDual
-                                      (Foldable__Either_foldMap (Data.SemigroupInternal.Mk_Dual GHC.Base.∘
-                                                                 (Data.SemigroupInternal.Mk_Endo GHC.Base.∘
-                                                                  GHC.Base.flip f)) t)) z.
+      appEndo (getDual (Foldable__Either_foldMap (Mk_Dual GHC.Base.∘
+                                                  (Mk_Endo GHC.Base.∘ GHC.Base.flip f)) t)) z.
 
 #[local] Definition Foldable__Either_foldr' {inst_a : Type}
    : forall {a : Type},
@@ -1270,15 +662,13 @@ Program Instance Foldable__NonEmpty : Foldable GHC.Base.NonEmpty :=
    : forall {a : Type},
      forall `{GHC.Num.Num a}, Data.Either.Either inst_a a -> a :=
   fun {a : Type} `{GHC.Num.Num a} =>
-    Coq.Program.Basics.compose Data.SemigroupInternal.getProduct
-                               (Foldable__Either_foldMap Data.SemigroupInternal.Mk_Product).
+    Coq.Program.Basics.compose getProduct (Foldable__Either_foldMap Mk_Product).
 
 #[local] Definition Foldable__Either_sum {inst_a : Type}
    : forall {a : Type},
      forall `{GHC.Num.Num a}, Data.Either.Either inst_a a -> a :=
   fun {a : Type} `{GHC.Num.Num a} =>
-    Coq.Program.Basics.compose Data.SemigroupInternal.getSum
-                               (Foldable__Either_foldMap Data.SemigroupInternal.Mk_Sum).
+    Coq.Program.Basics.compose getSum (Foldable__Either_foldMap Mk_Sum).
 
 #[local] Definition Foldable__Either_toList {inst_a : Type}
    : forall {a : Type}, Data.Either.Either inst_a a -> list a :=
@@ -1346,10 +736,8 @@ Program Instance Foldable__Either {a : Type}
      forall {a : Type}, (b -> a -> b) -> b -> GHC.Tuple.pair_type inst_a a -> b :=
   fun {b : Type} {a : Type} =>
     fun f z t =>
-      Data.SemigroupInternal.appEndo (Data.SemigroupInternal.getDual
-                                      (Foldable__pair_type_foldMap (Data.SemigroupInternal.Mk_Dual GHC.Base.∘
-                                                                    (Data.SemigroupInternal.Mk_Endo GHC.Base.∘
-                                                                     GHC.Base.flip f)) t)) z.
+      appEndo (getDual (Foldable__pair_type_foldMap (Mk_Dual GHC.Base.∘
+                                                     (Mk_Endo GHC.Base.∘ GHC.Base.flip f)) t)) z.
 
 #[local] Definition Foldable__pair_type_foldr' {inst_a : Type}
    : forall {a : Type},
@@ -1371,15 +759,13 @@ Program Instance Foldable__Either {a : Type}
    : forall {a : Type},
      forall `{GHC.Num.Num a}, GHC.Tuple.pair_type inst_a a -> a :=
   fun {a : Type} `{GHC.Num.Num a} =>
-    Coq.Program.Basics.compose Data.SemigroupInternal.getProduct
-                               (Foldable__pair_type_foldMap Data.SemigroupInternal.Mk_Product).
+    Coq.Program.Basics.compose getProduct (Foldable__pair_type_foldMap Mk_Product).
 
 #[local] Definition Foldable__pair_type_sum {inst_a : Type}
    : forall {a : Type},
      forall `{GHC.Num.Num a}, GHC.Tuple.pair_type inst_a a -> a :=
   fun {a : Type} `{GHC.Num.Num a} =>
-    Coq.Program.Basics.compose Data.SemigroupInternal.getSum
-                               (Foldable__pair_type_foldMap Data.SemigroupInternal.Mk_Sum).
+    Coq.Program.Basics.compose getSum (Foldable__pair_type_foldMap Mk_Sum).
 
 #[local] Definition Foldable__pair_type_toList {inst_a : Type}
    : forall {a : Type}, GHC.Tuple.pair_type inst_a a -> list a :=
@@ -1502,71 +888,61 @@ Program Instance Foldable__Proxy : Foldable Data.Proxy.Proxy :=
 
 #[local] Definition Foldable__Dual_foldMap
    : forall {m : Type},
-     forall {a : Type},
-     forall `{GHC.Base.Monoid m}, (a -> m) -> Data.SemigroupInternal.Dual a -> m :=
+     forall {a : Type}, forall `{GHC.Base.Monoid m}, (a -> m) -> Dual a -> m :=
   fun {m : Type} {a : Type} `{GHC.Base.Monoid m} => GHC.Prim.coerce.
 
 #[local] Definition Foldable__Dual_fold
-   : forall {m : Type},
-     forall `{GHC.Base.Monoid m}, Data.SemigroupInternal.Dual m -> m :=
+   : forall {m : Type}, forall `{GHC.Base.Monoid m}, Dual m -> m :=
   fun {m : Type} `{GHC.Base.Monoid m} => Foldable__Dual_foldMap GHC.Base.id.
 
 #[local] Definition Foldable__Dual_foldl'
-   : forall {b : Type},
-     forall {a : Type}, (b -> a -> b) -> b -> Data.SemigroupInternal.Dual a -> b :=
+   : forall {b : Type}, forall {a : Type}, (b -> a -> b) -> b -> Dual a -> b :=
   fun {b : Type} {a : Type} => GHC.Prim.coerce.
 
 #[local] Definition Foldable__Dual_foldMap'
    : forall {m : Type},
-     forall {a : Type},
-     forall `{GHC.Base.Monoid m}, (a -> m) -> Data.SemigroupInternal.Dual a -> m :=
+     forall {a : Type}, forall `{GHC.Base.Monoid m}, (a -> m) -> Dual a -> m :=
   fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
     fun f =>
       Foldable__Dual_foldl' (fun acc a => acc GHC.Base.<<>> f a) GHC.Base.mempty.
 
 #[local] Definition Foldable__Dual_foldl
-   : forall {b : Type},
-     forall {a : Type}, (b -> a -> b) -> b -> Data.SemigroupInternal.Dual a -> b :=
+   : forall {b : Type}, forall {a : Type}, (b -> a -> b) -> b -> Dual a -> b :=
   fun {b : Type} {a : Type} => GHC.Prim.coerce.
 
 #[local] Definition Foldable__Dual_foldr
-   : forall {a : Type},
-     forall {b : Type}, (a -> b -> b) -> b -> Data.SemigroupInternal.Dual a -> b :=
+   : forall {a : Type}, forall {b : Type}, (a -> b -> b) -> b -> Dual a -> b :=
   fun {a : Type} {b : Type} =>
     fun arg_0__ arg_1__ arg_2__ =>
       match arg_0__, arg_1__, arg_2__ with
-      | f, z, Data.SemigroupInternal.Mk_Dual x => f x z
+      | f, z, Mk_Dual x => f x z
       end.
 
 #[local] Definition Foldable__Dual_foldr'
-   : forall {a : Type},
-     forall {b : Type}, (a -> b -> b) -> b -> Data.SemigroupInternal.Dual a -> b :=
+   : forall {a : Type}, forall {b : Type}, (a -> b -> b) -> b -> Dual a -> b :=
   fun {a : Type} {b : Type} => Foldable__Dual_foldr.
 
 #[local] Definition Foldable__Dual_length
-   : forall {a : Type}, Data.SemigroupInternal.Dual a -> GHC.Num.Int :=
+   : forall {a : Type}, Dual a -> GHC.Num.Int :=
   fun {a : Type} => fun arg_0__ => #1.
 
-#[local] Definition Foldable__Dual_null
-   : forall {a : Type}, Data.SemigroupInternal.Dual a -> bool :=
+#[local] Definition Foldable__Dual_null : forall {a : Type}, Dual a -> bool :=
   fun {a : Type} => fun arg_0__ => false.
 
 #[local] Definition Foldable__Dual_product
-   : forall {a : Type},
-     forall `{GHC.Num.Num a}, Data.SemigroupInternal.Dual a -> a :=
-  fun {a : Type} `{GHC.Num.Num a} => Data.SemigroupInternal.getDual.
+   : forall {a : Type}, forall `{GHC.Num.Num a}, Dual a -> a :=
+  fun {a : Type} `{GHC.Num.Num a} => getDual.
 
 #[local] Definition Foldable__Dual_sum
-   : forall {a : Type},
-     forall `{GHC.Num.Num a}, Data.SemigroupInternal.Dual a -> a :=
-  fun {a : Type} `{GHC.Num.Num a} => Data.SemigroupInternal.getDual.
+   : forall {a : Type}, forall `{GHC.Num.Num a}, Dual a -> a :=
+  fun {a : Type} `{GHC.Num.Num a} => getDual.
 
 #[local] Definition Foldable__Dual_toList
-   : forall {a : Type}, Data.SemigroupInternal.Dual a -> list a :=
-  fun {a : Type} => fun '(Data.SemigroupInternal.Mk_Dual x) => cons x nil.
+   : forall {a : Type}, Dual a -> list a :=
+  fun {a : Type} => fun '(Mk_Dual x) => cons x nil.
 
 #[global]
-Program Instance Foldable__Dual : Foldable Data.SemigroupInternal.Dual :=
+Program Instance Foldable__Dual : Foldable Dual :=
   fun _ k__ =>
     k__ {| fold__ := fun {m : Type} `{GHC.Base.Monoid m} => Foldable__Dual_fold ;
            foldMap__ := fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
@@ -1585,71 +961,60 @@ Program Instance Foldable__Dual : Foldable Data.SemigroupInternal.Dual :=
 
 #[local] Definition Foldable__Sum_foldMap
    : forall {m : Type},
-     forall {a : Type},
-     forall `{GHC.Base.Monoid m}, (a -> m) -> Data.SemigroupInternal.Sum a -> m :=
+     forall {a : Type}, forall `{GHC.Base.Monoid m}, (a -> m) -> Sum a -> m :=
   fun {m : Type} {a : Type} `{GHC.Base.Monoid m} => GHC.Prim.coerce.
 
 #[local] Definition Foldable__Sum_fold
-   : forall {m : Type},
-     forall `{GHC.Base.Monoid m}, Data.SemigroupInternal.Sum m -> m :=
+   : forall {m : Type}, forall `{GHC.Base.Monoid m}, Sum m -> m :=
   fun {m : Type} `{GHC.Base.Monoid m} => Foldable__Sum_foldMap GHC.Base.id.
 
 #[local] Definition Foldable__Sum_foldl'
-   : forall {b : Type},
-     forall {a : Type}, (b -> a -> b) -> b -> Data.SemigroupInternal.Sum a -> b :=
+   : forall {b : Type}, forall {a : Type}, (b -> a -> b) -> b -> Sum a -> b :=
   fun {b : Type} {a : Type} => GHC.Prim.coerce.
 
 #[local] Definition Foldable__Sum_foldMap'
    : forall {m : Type},
-     forall {a : Type},
-     forall `{GHC.Base.Monoid m}, (a -> m) -> Data.SemigroupInternal.Sum a -> m :=
+     forall {a : Type}, forall `{GHC.Base.Monoid m}, (a -> m) -> Sum a -> m :=
   fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
     fun f =>
       Foldable__Sum_foldl' (fun acc a => acc GHC.Base.<<>> f a) GHC.Base.mempty.
 
 #[local] Definition Foldable__Sum_foldl
-   : forall {b : Type},
-     forall {a : Type}, (b -> a -> b) -> b -> Data.SemigroupInternal.Sum a -> b :=
+   : forall {b : Type}, forall {a : Type}, (b -> a -> b) -> b -> Sum a -> b :=
   fun {b : Type} {a : Type} => GHC.Prim.coerce.
 
 #[local] Definition Foldable__Sum_foldr
-   : forall {a : Type},
-     forall {b : Type}, (a -> b -> b) -> b -> Data.SemigroupInternal.Sum a -> b :=
+   : forall {a : Type}, forall {b : Type}, (a -> b -> b) -> b -> Sum a -> b :=
   fun {a : Type} {b : Type} =>
     fun arg_0__ arg_1__ arg_2__ =>
       match arg_0__, arg_1__, arg_2__ with
-      | f, z, Data.SemigroupInternal.Mk_Sum x => f x z
+      | f, z, Mk_Sum x => f x z
       end.
 
 #[local] Definition Foldable__Sum_foldr'
-   : forall {a : Type},
-     forall {b : Type}, (a -> b -> b) -> b -> Data.SemigroupInternal.Sum a -> b :=
+   : forall {a : Type}, forall {b : Type}, (a -> b -> b) -> b -> Sum a -> b :=
   fun {a : Type} {b : Type} => Foldable__Sum_foldr.
 
 #[local] Definition Foldable__Sum_length
-   : forall {a : Type}, Data.SemigroupInternal.Sum a -> GHC.Num.Int :=
+   : forall {a : Type}, Sum a -> GHC.Num.Int :=
   fun {a : Type} => fun arg_0__ => #1.
 
-#[local] Definition Foldable__Sum_null
-   : forall {a : Type}, Data.SemigroupInternal.Sum a -> bool :=
+#[local] Definition Foldable__Sum_null : forall {a : Type}, Sum a -> bool :=
   fun {a : Type} => fun arg_0__ => false.
 
 #[local] Definition Foldable__Sum_product
-   : forall {a : Type},
-     forall `{GHC.Num.Num a}, Data.SemigroupInternal.Sum a -> a :=
-  fun {a : Type} `{GHC.Num.Num a} => Data.SemigroupInternal.getSum.
+   : forall {a : Type}, forall `{GHC.Num.Num a}, Sum a -> a :=
+  fun {a : Type} `{GHC.Num.Num a} => getSum.
 
 #[local] Definition Foldable__Sum_sum
-   : forall {a : Type},
-     forall `{GHC.Num.Num a}, Data.SemigroupInternal.Sum a -> a :=
-  fun {a : Type} `{GHC.Num.Num a} => Data.SemigroupInternal.getSum.
+   : forall {a : Type}, forall `{GHC.Num.Num a}, Sum a -> a :=
+  fun {a : Type} `{GHC.Num.Num a} => getSum.
 
-#[local] Definition Foldable__Sum_toList
-   : forall {a : Type}, Data.SemigroupInternal.Sum a -> list a :=
-  fun {a : Type} => fun '(Data.SemigroupInternal.Mk_Sum x) => cons x nil.
+#[local] Definition Foldable__Sum_toList : forall {a : Type}, Sum a -> list a :=
+  fun {a : Type} => fun '(Mk_Sum x) => cons x nil.
 
 #[global]
-Program Instance Foldable__Sum : Foldable Data.SemigroupInternal.Sum :=
+Program Instance Foldable__Sum : Foldable Sum :=
   fun _ k__ =>
     k__ {| fold__ := fun {m : Type} `{GHC.Base.Monoid m} => Foldable__Sum_fold ;
            foldMap__ := fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
@@ -1668,77 +1033,62 @@ Program Instance Foldable__Sum : Foldable Data.SemigroupInternal.Sum :=
 
 #[local] Definition Foldable__Product_foldMap
    : forall {m : Type},
-     forall {a : Type},
-     forall `{GHC.Base.Monoid m},
-     (a -> m) -> Data.SemigroupInternal.Product a -> m :=
+     forall {a : Type}, forall `{GHC.Base.Monoid m}, (a -> m) -> Product a -> m :=
   fun {m : Type} {a : Type} `{GHC.Base.Monoid m} => GHC.Prim.coerce.
 
 #[local] Definition Foldable__Product_fold
-   : forall {m : Type},
-     forall `{GHC.Base.Monoid m}, Data.SemigroupInternal.Product m -> m :=
+   : forall {m : Type}, forall `{GHC.Base.Monoid m}, Product m -> m :=
   fun {m : Type} `{GHC.Base.Monoid m} => Foldable__Product_foldMap GHC.Base.id.
 
 #[local] Definition Foldable__Product_foldl'
-   : forall {b : Type},
-     forall {a : Type},
-     (b -> a -> b) -> b -> Data.SemigroupInternal.Product a -> b :=
+   : forall {b : Type}, forall {a : Type}, (b -> a -> b) -> b -> Product a -> b :=
   fun {b : Type} {a : Type} => GHC.Prim.coerce.
 
 #[local] Definition Foldable__Product_foldMap'
    : forall {m : Type},
-     forall {a : Type},
-     forall `{GHC.Base.Monoid m},
-     (a -> m) -> Data.SemigroupInternal.Product a -> m :=
+     forall {a : Type}, forall `{GHC.Base.Monoid m}, (a -> m) -> Product a -> m :=
   fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
     fun f =>
       Foldable__Product_foldl' (fun acc a => acc GHC.Base.<<>> f a) GHC.Base.mempty.
 
 #[local] Definition Foldable__Product_foldl
-   : forall {b : Type},
-     forall {a : Type},
-     (b -> a -> b) -> b -> Data.SemigroupInternal.Product a -> b :=
+   : forall {b : Type}, forall {a : Type}, (b -> a -> b) -> b -> Product a -> b :=
   fun {b : Type} {a : Type} => GHC.Prim.coerce.
 
 #[local] Definition Foldable__Product_foldr
-   : forall {a : Type},
-     forall {b : Type},
-     (a -> b -> b) -> b -> Data.SemigroupInternal.Product a -> b :=
+   : forall {a : Type}, forall {b : Type}, (a -> b -> b) -> b -> Product a -> b :=
   fun {a : Type} {b : Type} =>
     fun arg_0__ arg_1__ arg_2__ =>
       match arg_0__, arg_1__, arg_2__ with
-      | f, z, Data.SemigroupInternal.Mk_Product x => f x z
+      | f, z, Mk_Product x => f x z
       end.
 
 #[local] Definition Foldable__Product_foldr'
-   : forall {a : Type},
-     forall {b : Type},
-     (a -> b -> b) -> b -> Data.SemigroupInternal.Product a -> b :=
+   : forall {a : Type}, forall {b : Type}, (a -> b -> b) -> b -> Product a -> b :=
   fun {a : Type} {b : Type} => Foldable__Product_foldr.
 
 #[local] Definition Foldable__Product_length
-   : forall {a : Type}, Data.SemigroupInternal.Product a -> GHC.Num.Int :=
+   : forall {a : Type}, Product a -> GHC.Num.Int :=
   fun {a : Type} => fun arg_0__ => #1.
 
 #[local] Definition Foldable__Product_null
-   : forall {a : Type}, Data.SemigroupInternal.Product a -> bool :=
+   : forall {a : Type}, Product a -> bool :=
   fun {a : Type} => fun arg_0__ => false.
 
 #[local] Definition Foldable__Product_product
-   : forall {a : Type},
-     forall `{GHC.Num.Num a}, Data.SemigroupInternal.Product a -> a :=
-  fun {a : Type} `{GHC.Num.Num a} => Data.SemigroupInternal.getProduct.
+   : forall {a : Type}, forall `{GHC.Num.Num a}, Product a -> a :=
+  fun {a : Type} `{GHC.Num.Num a} => getProduct.
 
 #[local] Definition Foldable__Product_sum
-   : forall {a : Type},
-     forall `{GHC.Num.Num a}, Data.SemigroupInternal.Product a -> a :=
-  fun {a : Type} `{GHC.Num.Num a} => Data.SemigroupInternal.getProduct.
+   : forall {a : Type}, forall `{GHC.Num.Num a}, Product a -> a :=
+  fun {a : Type} `{GHC.Num.Num a} => getProduct.
 
 #[local] Definition Foldable__Product_toList
-   : forall {a : Type}, Data.SemigroupInternal.Product a -> list a :=
-  fun {a : Type} => fun '(Data.SemigroupInternal.Mk_Product x) => cons x nil.
+   : forall {a : Type}, Product a -> list a :=
+  fun {a : Type} => fun '(Mk_Product x) => cons x nil.
 
 #[global]
-Program Instance Foldable__Product : Foldable Data.SemigroupInternal.Product :=
+Program Instance Foldable__Product : Foldable Product :=
   fun _ k__ =>
     k__ {| fold__ := fun {m : Type} `{GHC.Base.Monoid m} => Foldable__Product_fold ;
            foldMap__ := fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
@@ -1764,33 +1114,27 @@ Program Instance Foldable__Product : Foldable Data.SemigroupInternal.Product :=
 #[local] Definition Foldable__Alt_foldMap {inst_f : Type -> Type} `{(Foldable
    inst_f)}
    : forall {m : Type},
-     forall {a : Type},
-     forall `{GHC.Base.Monoid m},
-     (a -> m) -> Data.SemigroupInternal.Alt inst_f a -> m :=
+     forall {a : Type}, forall `{GHC.Base.Monoid m}, (a -> m) -> Alt inst_f a -> m :=
   fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
-    fun f => foldMap f GHC.Base.∘ Data.SemigroupInternal.getAlt.
+    fun f => foldMap f GHC.Base.∘ getAlt.
 
 #[local] Definition Foldable__Alt_fold {inst_f : Type -> Type} `{(Foldable
    inst_f)}
-   : forall {m : Type},
-     forall `{GHC.Base.Monoid m}, Data.SemigroupInternal.Alt inst_f m -> m :=
+   : forall {m : Type}, forall `{GHC.Base.Monoid m}, Alt inst_f m -> m :=
   fun {m : Type} `{GHC.Base.Monoid m} => Foldable__Alt_foldMap GHC.Base.id.
 
 #[local] Definition Foldable__Alt_foldr {inst_f : Type -> Type} `{(Foldable
    inst_f)}
    : forall {a : Type},
-     forall {b : Type},
-     (a -> b -> b) -> b -> Data.SemigroupInternal.Alt inst_f a -> b :=
+     forall {b : Type}, (a -> b -> b) -> b -> Alt inst_f a -> b :=
   fun {a : Type} {b : Type} =>
     fun f z t =>
-      Data.SemigroupInternal.appEndo (Foldable__Alt_foldMap
-                                      (Coq.Program.Basics.compose Data.SemigroupInternal.Mk_Endo f) t) z.
+      appEndo (Foldable__Alt_foldMap (Coq.Program.Basics.compose Mk_Endo f) t) z.
 
 #[local] Definition Foldable__Alt_foldl' {inst_f : Type -> Type} `{(Foldable
    inst_f)}
    : forall {b : Type},
-     forall {a : Type},
-     (b -> a -> b) -> b -> Data.SemigroupInternal.Alt inst_f a -> b :=
+     forall {a : Type}, (b -> a -> b) -> b -> Alt inst_f a -> b :=
   fun {b : Type} {a : Type} =>
     fun f z0 xs =>
       let f' := fun x k z => k (f z x) in Foldable__Alt_foldr f' GHC.Base.id xs z0.
@@ -1798,9 +1142,7 @@ Program Instance Foldable__Product : Foldable Data.SemigroupInternal.Product :=
 #[local] Definition Foldable__Alt_foldMap' {inst_f : Type -> Type} `{(Foldable
    inst_f)}
    : forall {m : Type},
-     forall {a : Type},
-     forall `{GHC.Base.Monoid m},
-     (a -> m) -> Data.SemigroupInternal.Alt inst_f a -> m :=
+     forall {a : Type}, forall `{GHC.Base.Monoid m}, (a -> m) -> Alt inst_f a -> m :=
   fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
     fun f =>
       Foldable__Alt_foldl' (fun acc a => acc GHC.Base.<<>> f a) GHC.Base.mempty.
@@ -1808,27 +1150,23 @@ Program Instance Foldable__Product : Foldable Data.SemigroupInternal.Product :=
 #[local] Definition Foldable__Alt_foldl {inst_f : Type -> Type} `{(Foldable
    inst_f)}
    : forall {b : Type},
-     forall {a : Type},
-     (b -> a -> b) -> b -> Data.SemigroupInternal.Alt inst_f a -> b :=
+     forall {a : Type}, (b -> a -> b) -> b -> Alt inst_f a -> b :=
   fun {b : Type} {a : Type} =>
     fun f z t =>
-      Data.SemigroupInternal.appEndo (Data.SemigroupInternal.getDual
-                                      (Foldable__Alt_foldMap (Data.SemigroupInternal.Mk_Dual GHC.Base.∘
-                                                              (Data.SemigroupInternal.Mk_Endo GHC.Base.∘
-                                                               GHC.Base.flip f)) t)) z.
+      appEndo (getDual (Foldable__Alt_foldMap (Mk_Dual GHC.Base.∘
+                                               (Mk_Endo GHC.Base.∘ GHC.Base.flip f)) t)) z.
 
 #[local] Definition Foldable__Alt_foldr' {inst_f : Type -> Type} `{(Foldable
    inst_f)}
    : forall {a : Type},
-     forall {b : Type},
-     (a -> b -> b) -> b -> Data.SemigroupInternal.Alt inst_f a -> b :=
+     forall {b : Type}, (a -> b -> b) -> b -> Alt inst_f a -> b :=
   fun {a : Type} {b : Type} =>
     fun f z0 xs =>
       let f' := fun k x z => k (f x z) in Foldable__Alt_foldl f' GHC.Base.id xs z0.
 
 #[local] Definition Foldable__Alt_length {inst_f : Type -> Type} `{(Foldable
    inst_f)}
-   : forall {a : Type}, Data.SemigroupInternal.Alt inst_f a -> GHC.Num.Int :=
+   : forall {a : Type}, Alt inst_f a -> GHC.Num.Int :=
   fun {a : Type} =>
     Foldable__Alt_foldl' (fun arg_0__ arg_1__ =>
                             match arg_0__, arg_1__ with
@@ -1837,34 +1175,30 @@ Program Instance Foldable__Product : Foldable Data.SemigroupInternal.Product :=
 
 #[local] Definition Foldable__Alt_null {inst_f : Type -> Type} `{(Foldable
    inst_f)}
-   : forall {a : Type}, Data.SemigroupInternal.Alt inst_f a -> bool :=
+   : forall {a : Type}, Alt inst_f a -> bool :=
   fun {a : Type} => Foldable__Alt_foldr (fun arg_0__ arg_1__ => false) true.
 
 #[local] Definition Foldable__Alt_product {inst_f : Type -> Type} `{(Foldable
    inst_f)}
-   : forall {a : Type},
-     forall `{GHC.Num.Num a}, Data.SemigroupInternal.Alt inst_f a -> a :=
+   : forall {a : Type}, forall `{GHC.Num.Num a}, Alt inst_f a -> a :=
   fun {a : Type} `{GHC.Num.Num a} =>
-    Coq.Program.Basics.compose Data.SemigroupInternal.getProduct
-                               (Foldable__Alt_foldMap Data.SemigroupInternal.Mk_Product).
+    Coq.Program.Basics.compose getProduct (Foldable__Alt_foldMap Mk_Product).
 
 #[local] Definition Foldable__Alt_sum {inst_f : Type -> Type} `{(Foldable
    inst_f)}
-   : forall {a : Type},
-     forall `{GHC.Num.Num a}, Data.SemigroupInternal.Alt inst_f a -> a :=
+   : forall {a : Type}, forall `{GHC.Num.Num a}, Alt inst_f a -> a :=
   fun {a : Type} `{GHC.Num.Num a} =>
-    Coq.Program.Basics.compose Data.SemigroupInternal.getSum (Foldable__Alt_foldMap
-                                Data.SemigroupInternal.Mk_Sum).
+    Coq.Program.Basics.compose getSum (Foldable__Alt_foldMap Mk_Sum).
 
 #[local] Definition Foldable__Alt_toList {inst_f : Type -> Type} `{(Foldable
    inst_f)}
-   : forall {a : Type}, Data.SemigroupInternal.Alt inst_f a -> list a :=
+   : forall {a : Type}, Alt inst_f a -> list a :=
   fun {a : Type} =>
     fun t => GHC.Base.build' (fun _ => (fun c n => Foldable__Alt_foldr c n t)).
 
 #[global]
 Program Instance Foldable__Alt {f : Type -> Type} `{(Foldable f)}
-   : Foldable (Data.SemigroupInternal.Alt f) :=
+   : Foldable (Alt f) :=
   fun _ k__ =>
     k__ {| fold__ := fun {m : Type} `{GHC.Base.Monoid m} => Foldable__Alt_fold ;
            foldMap__ := fun {m : Type} {a : Type} `{GHC.Base.Monoid m} =>
@@ -1901,8 +1235,7 @@ Program Instance Foldable__Alt {f : Type -> Type} `{(Foldable f)}
      forall {b : Type}, (a -> b -> b) -> b -> Data.Monoid.Ap inst_f a -> b :=
   fun {a : Type} {b : Type} =>
     fun f z t =>
-      Data.SemigroupInternal.appEndo (Foldable__Ap_foldMap (Coq.Program.Basics.compose
-                                                            Data.SemigroupInternal.Mk_Endo f) t) z.
+      appEndo (Foldable__Ap_foldMap (Coq.Program.Basics.compose Mk_Endo f) t) z.
 
 #[local] Definition Foldable__Ap_foldl' {inst_f : Type -> Type} `{(Foldable
    inst_f)}
@@ -1927,10 +1260,8 @@ Program Instance Foldable__Alt {f : Type -> Type} `{(Foldable f)}
      forall {a : Type}, (b -> a -> b) -> b -> Data.Monoid.Ap inst_f a -> b :=
   fun {b : Type} {a : Type} =>
     fun f z t =>
-      Data.SemigroupInternal.appEndo (Data.SemigroupInternal.getDual
-                                      (Foldable__Ap_foldMap (Data.SemigroupInternal.Mk_Dual GHC.Base.∘
-                                                             (Data.SemigroupInternal.Mk_Endo GHC.Base.∘
-                                                              GHC.Base.flip f)) t)) z.
+      appEndo (getDual (Foldable__Ap_foldMap (Mk_Dual GHC.Base.∘
+                                              (Mk_Endo GHC.Base.∘ GHC.Base.flip f)) t)) z.
 
 #[local] Definition Foldable__Ap_foldr' {inst_f : Type -> Type} `{(Foldable
    inst_f)}
@@ -1958,15 +1289,13 @@ Program Instance Foldable__Alt {f : Type -> Type} `{(Foldable f)}
    inst_f)}
    : forall {a : Type}, forall `{GHC.Num.Num a}, Data.Monoid.Ap inst_f a -> a :=
   fun {a : Type} `{GHC.Num.Num a} =>
-    Coq.Program.Basics.compose Data.SemigroupInternal.getProduct
-                               (Foldable__Ap_foldMap Data.SemigroupInternal.Mk_Product).
+    Coq.Program.Basics.compose getProduct (Foldable__Ap_foldMap Mk_Product).
 
 #[local] Definition Foldable__Ap_sum {inst_f : Type -> Type} `{(Foldable
    inst_f)}
    : forall {a : Type}, forall `{GHC.Num.Num a}, Data.Monoid.Ap inst_f a -> a :=
   fun {a : Type} `{GHC.Num.Num a} =>
-    Coq.Program.Basics.compose Data.SemigroupInternal.getSum (Foldable__Ap_foldMap
-                                Data.SemigroupInternal.Mk_Sum).
+    Coq.Program.Basics.compose getSum (Foldable__Ap_foldMap Mk_Sum).
 
 #[local] Definition Foldable__Ap_toList {inst_f : Type -> Type} `{(Foldable
    inst_f)}
@@ -2055,24 +1384,22 @@ Program Instance Foldable__Ap {f : Type -> Type} `{(Foldable f)}
                        fun c n => foldr (fun x y => (@foldr _ Foldable__list _ _ c y x)) n xs).
 
 #[global] Definition and {t : Type -> Type} `{Foldable t} : t bool -> bool :=
-  Coq.Program.Basics.compose Data.SemigroupInternal.getAll (foldMap
-                              Data.SemigroupInternal.Mk_All).
+  Coq.Program.Basics.compose getAll (foldMap Mk_All).
 
 #[global] Definition or {t : Type -> Type} `{Foldable t} : t bool -> bool :=
-  Coq.Program.Basics.compose Data.SemigroupInternal.getAny (foldMap
-                              Data.SemigroupInternal.Mk_Any).
+  Coq.Program.Basics.compose getAny (foldMap Mk_Any).
 
 #[global] Definition any {t : Type -> Type} {a : Type} `{Foldable t}
    : (a -> bool) -> t a -> bool :=
   fun p =>
-    Coq.Program.Basics.compose Data.SemigroupInternal.getAny (foldMap
-                                (Coq.Program.Basics.compose Data.SemigroupInternal.Mk_Any p)).
+    Coq.Program.Basics.compose getAny (foldMap (Coq.Program.Basics.compose Mk_Any
+                                                                           p)).
 
 #[global] Definition all {t : Type -> Type} {a : Type} `{Foldable t}
    : (a -> bool) -> t a -> bool :=
   fun p =>
-    Coq.Program.Basics.compose Data.SemigroupInternal.getAll (foldMap
-                                (Coq.Program.Basics.compose Data.SemigroupInternal.Mk_All p)).
+    Coq.Program.Basics.compose getAll (foldMap (Coq.Program.Basics.compose Mk_All
+                                                                           p)).
 
 (* Skipping definition `Data.Foldable.maximumBy' *)
 
@@ -2094,25 +1421,18 @@ Program Instance Foldable__Ap {f : Type -> Type} `{(Foldable f)}
     foldMap (fun x => Data.Monoid.Mk_First (if p x : bool then Some x else None)).
 
 (* External variables:
-     None Some Type bool cons false list negb nil option pair true tt unit
-     Coq.Program.Basics.compose Data.Either.Either Data.Either.Left Data.Either.Right
-     Data.Either.isLeft Data.Maybe.maybe Data.Monoid.Ap Data.Monoid.Mk_First
-     Data.Monoid.getAp Data.Monoid.getFirst Data.Ord.Down Data.Ord.Mk_Down
-     Data.Proxy.Proxy Data.SemigroupInternal.Alt Data.SemigroupInternal.Dual
-     Data.SemigroupInternal.Mk_All Data.SemigroupInternal.Mk_Any
-     Data.SemigroupInternal.Mk_Dual Data.SemigroupInternal.Mk_Endo
-     Data.SemigroupInternal.Mk_Product Data.SemigroupInternal.Mk_Sum
-     Data.SemigroupInternal.Product Data.SemigroupInternal.Sum
-     Data.SemigroupInternal.appEndo Data.SemigroupInternal.getAll
-     Data.SemigroupInternal.getAlt Data.SemigroupInternal.getAny
-     Data.SemigroupInternal.getDual Data.SemigroupInternal.getProduct
-     Data.SemigroupInternal.getSum GHC.Base.Applicative GHC.Base.Eq_ GHC.Base.Monad
-     GHC.Base.Monoid GHC.Base.NEcons GHC.Base.NonEmpty GHC.Base.build' GHC.Base.flip
-     GHC.Base.foldl GHC.Base.foldl' GHC.Base.foldr GHC.Base.id GHC.Base.mappend
-     GHC.Base.mempty GHC.Base.op_z2218U__ GHC.Base.op_zeze__ GHC.Base.op_zgzg__
-     GHC.Base.op_zgzgze__ GHC.Base.op_zlzlzgzg__ GHC.Base.op_ztzg__ GHC.Base.pure
-     GHC.Base.return_ GHC.Generics.UAddr GHC.Generics.UChar GHC.Generics.UDouble
-     GHC.Generics.UFloat GHC.Generics.UInt GHC.Generics.UWord GHC.List.length
-     GHC.List.null GHC.List.product GHC.List.sum GHC.Num.Int GHC.Num.Num
-     GHC.Num.fromInteger GHC.Num.op_zp__ GHC.Prim.coerce GHC.Tuple.pair_type
+     Alt Dual Mk_All Mk_Any Mk_Dual Mk_Endo Mk_Product Mk_Sum None Product Some Sum
+     Type appEndo bool cons false getAll getAlt getAny getDual getProduct getSum list
+     negb nil option pair true tt unit Coq.Program.Basics.compose Data.Either.Either
+     Data.Either.Left Data.Either.Right Data.Either.isLeft Data.Maybe.maybe
+     Data.Monoid.Ap Data.Monoid.Mk_First Data.Monoid.getAp Data.Monoid.getFirst
+     Data.Ord.Down Data.Ord.Mk_Down Data.Proxy.Proxy GHC.Base.Applicative
+     GHC.Base.Eq_ GHC.Base.Monad GHC.Base.Monoid GHC.Base.NEcons GHC.Base.NonEmpty
+     GHC.Base.build' GHC.Base.flip GHC.Base.foldl GHC.Base.foldl' GHC.Base.foldr
+     GHC.Base.id GHC.Base.mappend GHC.Base.mempty GHC.Base.op_z2218U__
+     GHC.Base.op_zeze__ GHC.Base.op_zgzg__ GHC.Base.op_zgzgze__
+     GHC.Base.op_zlzlzgzg__ GHC.Base.op_ztzg__ GHC.Base.pure GHC.Base.return_
+     GHC.List.length GHC.List.null GHC.List.product GHC.List.sum GHC.Num.Int
+     GHC.Num.Num GHC.Num.fromInteger GHC.Num.op_zp__ GHC.Prim.coerce
+     GHC.Tuple.pair_type
 *)
diff --git a/base/Data/Functor/Compose.v b/base/Data/Functor/Compose.v
index d28b41df..097eea20 100644
--- a/base/Data/Functor/Compose.v
+++ b/base/Data/Functor/Compose.v
@@ -39,6 +39,15 @@ Arguments Mk_Compose {_} {_} {_} {_} {_} _.
 
 (* Converted value declarations: *)
 
+(* Skipping all instances of class `Data.Data.Data', including
+   `Data.Functor.Compose.Data__Compose' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic', including
+   `Data.Functor.Compose.Generic__Compose' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic1', including
+   `Data.Functor.Compose.Generic1__Compose__5' *)
+
 #[local] Definition Eq1__Compose_liftEq {inst_f : Type -> Type} {inst_g
    : Type -> Type} `{Data.Functor.Classes.Eq1 inst_f} `{Data.Functor.Classes.Eq1
   inst_g}
@@ -191,7 +200,7 @@ Program Instance Ord__Compose {f : Type -> Type} {g : Type -> Type} {a : Type}
     fun arg_0__ arg_1__ =>
       match arg_0__, arg_1__ with
       | a, Mk_Compose x =>
-          Mk_Compose (Functor__Compose_fmap (fun arg_2__ => a GHC.Base.<$ arg_2__) x)
+          Mk_Compose (GHC.Base.fmap (fun arg_2__ => a GHC.Base.<$ arg_2__) x)
       end.
 
 #[global]
diff --git a/base/Data/Functor/Const.v b/base/Data/Functor/Const.v
index de056ded..4dfafc11 100644
--- a/base/Data/Functor/Const.v
+++ b/base/Data/Functor/Const.v
@@ -46,6 +46,155 @@ Arguments Mk_Const {_} {_} {_} _.
 
 (* Converted value declarations: *)
 
+(* Skipping all instances of class `Data.Bits.Bits', including
+   `Data.Functor.Const.Bits__Const' *)
+
+(* Skipping all instances of class `GHC.Enum.Bounded', including
+   `Data.Functor.Const.Bounded__Const' *)
+
+(* Skipping all instances of class `GHC.Enum.Enum', including
+   `Data.Functor.Const.Enum__Const' *)
+
+Instance Unpeel_Const (k a : Type) (b : k)
+   : HsToCoq.Unpeel.Unpeel (Const a b) a :=
+  HsToCoq.Unpeel.Build_Unpeel _ _ getConst Mk_Const.
+
+#[local] Definition Eq___Const_op_zeze__ {inst_a : Type} {inst_k : Type} {inst_b
+   : inst_k} `{GHC.Base.Eq_ inst_a}
+   : Const inst_a inst_b -> Const inst_a inst_b -> bool :=
+  GHC.Prim.coerce (_GHC.Base.==_).
+
+#[local] Definition Eq___Const_op_zsze__ {inst_a : Type} {inst_k : Type} {inst_b
+   : inst_k} `{GHC.Base.Eq_ inst_a}
+   : Const inst_a inst_b -> Const inst_a inst_b -> bool :=
+  GHC.Prim.coerce (_GHC.Base./=_).
+
+#[global]
+Program Instance Eq___Const {a : Type} {k : Type} {b : k} `{GHC.Base.Eq_ a}
+   : GHC.Base.Eq_ (Const a b) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zeze____ := Eq___Const_op_zeze__ ;
+           GHC.Base.op_zsze____ := Eq___Const_op_zsze__ |}.
+
+(* Skipping all instances of class `Data.Bits.FiniteBits', including
+   `Data.Functor.Const.FiniteBits__Const' *)
+
+(* Skipping all instances of class `GHC.Float.Floating', including
+   `Data.Functor.Const.Floating__Const' *)
+
+(* Skipping all instances of class `GHC.Real.Fractional', including
+   `Data.Functor.Const.Fractional__Const' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic', including
+   `Data.Functor.Const.Generic__Const' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic1', including
+   `Data.Functor.Const.Generic1__Const__5' *)
+
+(* Skipping all instances of class `GHC.Real.Integral', including
+   `Data.Functor.Const.Integral__Const' *)
+
+(* Skipping all instances of class `GHC.Ix.Ix', including
+   `Data.Functor.Const.Ix__Const' *)
+
+#[local] Definition Semigroup__Const_op_zlzlzgzg__ {inst_a : Type} {inst_k
+   : Type} {inst_b : inst_k} `{GHC.Base.Semigroup inst_a}
+   : Const inst_a inst_b -> Const inst_a inst_b -> Const inst_a inst_b :=
+  GHC.Prim.coerce (_GHC.Base.<<>>_).
+
+#[global]
+Program Instance Semigroup__Const {a : Type} {k : Type} {b : k}
+  `{GHC.Base.Semigroup a}
+   : GHC.Base.Semigroup (Const a b) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zlzlzgzg____ := Semigroup__Const_op_zlzlzgzg__ |}.
+
+#[local] Definition Monoid__Const_mappend {inst_a : Type} {inst_k : Type}
+  {inst_b : inst_k} `{GHC.Base.Monoid inst_a}
+   : Const inst_a inst_b -> Const inst_a inst_b -> Const inst_a inst_b :=
+  GHC.Prim.coerce (GHC.Base.mappend).
+
+#[local] Definition Monoid__Const_mconcat {inst_a : Type} {inst_k : Type}
+  {inst_b : inst_k} `{GHC.Base.Monoid inst_a}
+   : list (Const inst_a inst_b) -> Const inst_a inst_b :=
+  GHC.Prim.coerce (GHC.Base.mconcat).
+
+#[local] Definition Monoid__Const_mempty {inst_a : Type} {inst_k : Type} {inst_b
+   : inst_k} `{GHC.Base.Monoid inst_a}
+   : Const inst_a inst_b :=
+  GHC.Prim.coerce (GHC.Base.mempty).
+
+#[global]
+Program Instance Monoid__Const {a : Type} {k : Type} {b : k} `{GHC.Base.Monoid
+  a}
+   : GHC.Base.Monoid (Const a b) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.mappend__ := Monoid__Const_mappend ;
+           GHC.Base.mconcat__ := Monoid__Const_mconcat ;
+           GHC.Base.mempty__ := Monoid__Const_mempty |}.
+
+(* Skipping all instances of class `GHC.Num.Num', including
+   `Data.Functor.Const.Num__Const' *)
+
+#[local] Definition Ord__Const_op_zl__ {inst_a : Type} {inst_k : Type} {inst_b
+   : inst_k} `{GHC.Base.Ord inst_a}
+   : Const inst_a inst_b -> Const inst_a inst_b -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<_).
+
+#[local] Definition Ord__Const_op_zlze__ {inst_a : Type} {inst_k : Type} {inst_b
+   : inst_k} `{GHC.Base.Ord inst_a}
+   : Const inst_a inst_b -> Const inst_a inst_b -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<=_).
+
+#[local] Definition Ord__Const_op_zg__ {inst_a : Type} {inst_k : Type} {inst_b
+   : inst_k} `{GHC.Base.Ord inst_a}
+   : Const inst_a inst_b -> Const inst_a inst_b -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>_).
+
+#[local] Definition Ord__Const_op_zgze__ {inst_a : Type} {inst_k : Type} {inst_b
+   : inst_k} `{GHC.Base.Ord inst_a}
+   : Const inst_a inst_b -> Const inst_a inst_b -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>=_).
+
+#[local] Definition Ord__Const_compare {inst_a : Type} {inst_k : Type} {inst_b
+   : inst_k} `{GHC.Base.Ord inst_a}
+   : Const inst_a inst_b -> Const inst_a inst_b -> comparison :=
+  GHC.Prim.coerce (GHC.Base.compare).
+
+#[local] Definition Ord__Const_max {inst_a : Type} {inst_k : Type} {inst_b
+   : inst_k} `{GHC.Base.Ord inst_a}
+   : Const inst_a inst_b -> Const inst_a inst_b -> Const inst_a inst_b :=
+  GHC.Prim.coerce (GHC.Base.max).
+
+#[local] Definition Ord__Const_min {inst_a : Type} {inst_k : Type} {inst_b
+   : inst_k} `{GHC.Base.Ord inst_a}
+   : Const inst_a inst_b -> Const inst_a inst_b -> Const inst_a inst_b :=
+  GHC.Prim.coerce (GHC.Base.min).
+
+#[global]
+Program Instance Ord__Const {a : Type} {k : Type} {b : k} `{GHC.Base.Ord a}
+   : GHC.Base.Ord (Const a b) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zl____ := Ord__Const_op_zl__ ;
+           GHC.Base.op_zlze____ := Ord__Const_op_zlze__ ;
+           GHC.Base.op_zg____ := Ord__Const_op_zg__ ;
+           GHC.Base.op_zgze____ := Ord__Const_op_zgze__ ;
+           GHC.Base.compare__ := Ord__Const_compare ;
+           GHC.Base.max__ := Ord__Const_max ;
+           GHC.Base.min__ := Ord__Const_min |}.
+
+(* Skipping all instances of class `GHC.Real.Real', including
+   `Data.Functor.Const.Real__Const' *)
+
+(* Skipping all instances of class `GHC.Real.RealFrac', including
+   `Data.Functor.Const.RealFrac__Const' *)
+
+(* Skipping all instances of class `GHC.Float.RealFloat', including
+   `Data.Functor.Const.RealFloat__Const' *)
+
+(* Skipping all instances of class `Foreign.Storable.Storable', including
+   `Data.Functor.Const.Storable__Const' *)
+
 (* Skipping all instances of class `GHC.Read.Read', including
    `Data.Functor.Const.Read__Const' *)
 
@@ -217,25 +366,27 @@ Program Instance Applicative__Const {m : Type} `{GHC.Base.Monoid m}
              Applicative__Const_op_ztzg__ ;
            GHC.Base.pure__ := fun {a : Type} => Applicative__Const_pure |}.
 
-Instance Unpeel_Const (k a : Type) (b : k)
-   : HsToCoq.Unpeel.Unpeel (Const a b) a :=
-  HsToCoq.Unpeel.Build_Unpeel _ _ getConst Mk_Const.
-
 (* External variables:
-     Type bool false list true Coq.Program.Basics.compose Data.Foldable.Foldable
-     Data.Foldable.foldMap'__ Data.Foldable.foldMap__ Data.Foldable.fold__
-     Data.Foldable.foldl'__ Data.Foldable.foldl__ Data.Foldable.foldr'__
-     Data.Foldable.foldr__ Data.Foldable.length__ Data.Foldable.null__
-     Data.Foldable.product__ Data.Foldable.sum__ Data.Foldable.toList__
-     Data.SemigroupInternal.Mk_Dual Data.SemigroupInternal.Mk_Endo
-     Data.SemigroupInternal.Mk_Product Data.SemigroupInternal.Mk_Sum
-     Data.SemigroupInternal.appEndo Data.SemigroupInternal.getDual
-     Data.SemigroupInternal.getProduct Data.SemigroupInternal.getSum
-     GHC.Base.Applicative GHC.Base.Functor GHC.Base.Monoid GHC.Base.build'
-     GHC.Base.const GHC.Base.flip GHC.Base.fmap__ GHC.Base.id GHC.Base.liftA2__
-     GHC.Base.mappend GHC.Base.mempty GHC.Base.op_z2218U__ GHC.Base.op_zlzd__
-     GHC.Base.op_zlzd____ GHC.Base.op_zlzlzgzg__ GHC.Base.op_zlztzg____
-     GHC.Base.op_ztzg____ GHC.Base.pure__ GHC.Num.Int GHC.Num.Num GHC.Num.fromInteger
-     GHC.Num.op_zp__ GHC.Prim.coerce HsToCoq.Unpeel.Build_Unpeel
-     HsToCoq.Unpeel.Unpeel
+     Type bool comparison false list true Coq.Program.Basics.compose
+     Data.Foldable.Foldable Data.Foldable.foldMap'__ Data.Foldable.foldMap__
+     Data.Foldable.fold__ Data.Foldable.foldl'__ Data.Foldable.foldl__
+     Data.Foldable.foldr'__ Data.Foldable.foldr__ Data.Foldable.length__
+     Data.Foldable.null__ Data.Foldable.product__ Data.Foldable.sum__
+     Data.Foldable.toList__ Data.SemigroupInternal.Mk_Dual
+     Data.SemigroupInternal.Mk_Endo Data.SemigroupInternal.Mk_Product
+     Data.SemigroupInternal.Mk_Sum Data.SemigroupInternal.appEndo
+     Data.SemigroupInternal.getDual Data.SemigroupInternal.getProduct
+     Data.SemigroupInternal.getSum GHC.Base.Applicative GHC.Base.Eq_ GHC.Base.Functor
+     GHC.Base.Monoid GHC.Base.Ord GHC.Base.Semigroup GHC.Base.build' GHC.Base.compare
+     GHC.Base.compare__ GHC.Base.const GHC.Base.flip GHC.Base.fmap__ GHC.Base.id
+     GHC.Base.liftA2__ GHC.Base.mappend GHC.Base.mappend__ GHC.Base.max
+     GHC.Base.max__ GHC.Base.mconcat GHC.Base.mconcat__ GHC.Base.mempty
+     GHC.Base.mempty__ GHC.Base.min GHC.Base.min__ GHC.Base.op_z2218U__
+     GHC.Base.op_zeze__ GHC.Base.op_zeze____ GHC.Base.op_zg__ GHC.Base.op_zg____
+     GHC.Base.op_zgze__ GHC.Base.op_zgze____ GHC.Base.op_zl__ GHC.Base.op_zl____
+     GHC.Base.op_zlzd__ GHC.Base.op_zlzd____ GHC.Base.op_zlze__ GHC.Base.op_zlze____
+     GHC.Base.op_zlzlzgzg__ GHC.Base.op_zlzlzgzg____ GHC.Base.op_zlztzg____
+     GHC.Base.op_zsze__ GHC.Base.op_zsze____ GHC.Base.op_ztzg____ GHC.Base.pure__
+     GHC.Num.Int GHC.Num.Num GHC.Num.fromInteger GHC.Num.op_zp__ GHC.Prim.coerce
+     HsToCoq.Unpeel.Build_Unpeel HsToCoq.Unpeel.Unpeel
 *)
diff --git a/base/Data/Functor/Identity.v b/base/Data/Functor/Identity.v
index 0fabb732..fa8dda86 100644
--- a/base/Data/Functor/Identity.v
+++ b/base/Data/Functor/Identity.v
@@ -36,6 +36,144 @@ Instance Unpeel_Identity a : HsToCoq.Unpeel.Unpeel (Identity a) a :=
 
 (* Converted value declarations: *)
 
+(* Skipping all instances of class `Data.Bits.Bits', including
+   `Data.Functor.Identity.Bits__Identity' *)
+
+(* Skipping all instances of class `GHC.Enum.Bounded', including
+   `Data.Functor.Identity.Bounded__Identity' *)
+
+(* Skipping all instances of class `GHC.Enum.Enum', including
+   `Data.Functor.Identity.Enum__Identity' *)
+
+#[local] Definition Eq___Identity_op_zeze__ {inst_a : Type} `{GHC.Base.Eq_
+  inst_a}
+   : Identity inst_a -> Identity inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.==_).
+
+#[local] Definition Eq___Identity_op_zsze__ {inst_a : Type} `{GHC.Base.Eq_
+  inst_a}
+   : Identity inst_a -> Identity inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base./=_).
+
+#[global]
+Program Instance Eq___Identity {a : Type} `{GHC.Base.Eq_ a}
+   : GHC.Base.Eq_ (Identity a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zeze____ := Eq___Identity_op_zeze__ ;
+           GHC.Base.op_zsze____ := Eq___Identity_op_zsze__ |}.
+
+(* Skipping all instances of class `Data.Bits.FiniteBits', including
+   `Data.Functor.Identity.FiniteBits__Identity' *)
+
+(* Skipping all instances of class `GHC.Float.Floating', including
+   `Data.Functor.Identity.Floating__Identity' *)
+
+(* Skipping all instances of class `GHC.Real.Fractional', including
+   `Data.Functor.Identity.Fractional__Identity' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic', including
+   `Data.Functor.Identity.Generic__Identity' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic1', including
+   `Data.Functor.Identity.Generic1__TYPE__Identity__LiftedRep' *)
+
+(* Skipping all instances of class `GHC.Real.Integral', including
+   `Data.Functor.Identity.Integral__Identity' *)
+
+(* Skipping all instances of class `GHC.Ix.Ix', including
+   `Data.Functor.Identity.Ix__Identity' *)
+
+#[local] Definition Semigroup__Identity_op_zlzlzgzg__ {inst_a : Type}
+  `{GHC.Base.Semigroup inst_a}
+   : Identity inst_a -> Identity inst_a -> Identity inst_a :=
+  GHC.Prim.coerce (_GHC.Base.<<>>_).
+
+#[global]
+Program Instance Semigroup__Identity {a : Type} `{GHC.Base.Semigroup a}
+   : GHC.Base.Semigroup (Identity a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zlzlzgzg____ := Semigroup__Identity_op_zlzlzgzg__ |}.
+
+#[local] Definition Monoid__Identity_mappend {inst_a : Type} `{GHC.Base.Monoid
+  inst_a}
+   : Identity inst_a -> Identity inst_a -> Identity inst_a :=
+  GHC.Prim.coerce (GHC.Base.mappend).
+
+#[local] Definition Monoid__Identity_mconcat {inst_a : Type} `{GHC.Base.Monoid
+  inst_a}
+   : list (Identity inst_a) -> Identity inst_a :=
+  GHC.Prim.coerce (GHC.Base.mconcat).
+
+#[local] Definition Monoid__Identity_mempty {inst_a : Type} `{GHC.Base.Monoid
+  inst_a}
+   : Identity inst_a :=
+  GHC.Prim.coerce (GHC.Base.mempty).
+
+#[global]
+Program Instance Monoid__Identity {a : Type} `{GHC.Base.Monoid a}
+   : GHC.Base.Monoid (Identity a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.mappend__ := Monoid__Identity_mappend ;
+           GHC.Base.mconcat__ := Monoid__Identity_mconcat ;
+           GHC.Base.mempty__ := Monoid__Identity_mempty |}.
+
+(* Skipping all instances of class `GHC.Num.Num', including
+   `Data.Functor.Identity.Num__Identity' *)
+
+#[local] Definition Ord__Identity_op_zl__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Identity inst_a -> Identity inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<_).
+
+#[local] Definition Ord__Identity_op_zlze__ {inst_a : Type} `{GHC.Base.Ord
+  inst_a}
+   : Identity inst_a -> Identity inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<=_).
+
+#[local] Definition Ord__Identity_op_zg__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Identity inst_a -> Identity inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>_).
+
+#[local] Definition Ord__Identity_op_zgze__ {inst_a : Type} `{GHC.Base.Ord
+  inst_a}
+   : Identity inst_a -> Identity inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>=_).
+
+#[local] Definition Ord__Identity_compare {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Identity inst_a -> Identity inst_a -> comparison :=
+  GHC.Prim.coerce (GHC.Base.compare).
+
+#[local] Definition Ord__Identity_max {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Identity inst_a -> Identity inst_a -> Identity inst_a :=
+  GHC.Prim.coerce (GHC.Base.max).
+
+#[local] Definition Ord__Identity_min {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Identity inst_a -> Identity inst_a -> Identity inst_a :=
+  GHC.Prim.coerce (GHC.Base.min).
+
+#[global]
+Program Instance Ord__Identity {a : Type} `{GHC.Base.Ord a}
+   : GHC.Base.Ord (Identity a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zl____ := Ord__Identity_op_zl__ ;
+           GHC.Base.op_zlze____ := Ord__Identity_op_zlze__ ;
+           GHC.Base.op_zg____ := Ord__Identity_op_zg__ ;
+           GHC.Base.op_zgze____ := Ord__Identity_op_zgze__ ;
+           GHC.Base.compare__ := Ord__Identity_compare ;
+           GHC.Base.max__ := Ord__Identity_max ;
+           GHC.Base.min__ := Ord__Identity_min |}.
+
+(* Skipping all instances of class `GHC.Real.Real', including
+   `Data.Functor.Identity.Real__Identity' *)
+
+(* Skipping all instances of class `GHC.Real.RealFrac', including
+   `Data.Functor.Identity.RealFrac__Identity' *)
+
+(* Skipping all instances of class `GHC.Float.RealFloat', including
+   `Data.Functor.Identity.RealFloat__Identity' *)
+
+(* Skipping all instances of class `Foreign.Storable.Storable', including
+   `Data.Functor.Identity.Storable__Identity' *)
+
 (* Skipping all instances of class `GHC.Read.Read', including
    `Data.Functor.Identity.Read__Identity' *)
 
@@ -200,15 +338,22 @@ Program Instance Monad__Identity : GHC.Base.Monad Identity :=
    `Data.Functor.Identity.MonadFix__Identity' *)
 
 (* External variables:
-     Type bool cons false list nil Data.Foldable.Foldable Data.Foldable.foldMap'__
-     Data.Foldable.foldMap__ Data.Foldable.fold__ Data.Foldable.foldl'__
-     Data.Foldable.foldl__ Data.Foldable.foldr'__ Data.Foldable.foldr__
-     Data.Foldable.length__ Data.Foldable.null__ Data.Foldable.product__
-     Data.Foldable.sum__ Data.Foldable.toList__ GHC.Base.Applicative GHC.Base.Functor
-     GHC.Base.Monad GHC.Base.Monoid GHC.Base.const GHC.Base.fmap__ GHC.Base.id
-     GHC.Base.liftA2__ GHC.Base.mempty GHC.Base.op_z2218U__ GHC.Base.op_zgzg____
-     GHC.Base.op_zgzgze____ GHC.Base.op_zlzd__ GHC.Base.op_zlzd____
-     GHC.Base.op_zlzlzgzg__ GHC.Base.op_zlztzg____ GHC.Base.op_ztzg____ GHC.Base.pure
+     Type bool comparison cons false list nil Data.Foldable.Foldable
+     Data.Foldable.foldMap'__ Data.Foldable.foldMap__ Data.Foldable.fold__
+     Data.Foldable.foldl'__ Data.Foldable.foldl__ Data.Foldable.foldr'__
+     Data.Foldable.foldr__ Data.Foldable.length__ Data.Foldable.null__
+     Data.Foldable.product__ Data.Foldable.sum__ Data.Foldable.toList__
+     GHC.Base.Applicative GHC.Base.Eq_ GHC.Base.Functor GHC.Base.Monad
+     GHC.Base.Monoid GHC.Base.Ord GHC.Base.Semigroup GHC.Base.compare
+     GHC.Base.compare__ GHC.Base.const GHC.Base.fmap__ GHC.Base.id GHC.Base.liftA2__
+     GHC.Base.mappend GHC.Base.mappend__ GHC.Base.max GHC.Base.max__ GHC.Base.mconcat
+     GHC.Base.mconcat__ GHC.Base.mempty GHC.Base.mempty__ GHC.Base.min GHC.Base.min__
+     GHC.Base.op_z2218U__ GHC.Base.op_zeze__ GHC.Base.op_zeze____ GHC.Base.op_zg__
+     GHC.Base.op_zg____ GHC.Base.op_zgze__ GHC.Base.op_zgze____ GHC.Base.op_zgzg____
+     GHC.Base.op_zgzgze____ GHC.Base.op_zl__ GHC.Base.op_zl____ GHC.Base.op_zlzd__
+     GHC.Base.op_zlzd____ GHC.Base.op_zlze__ GHC.Base.op_zlze____
+     GHC.Base.op_zlzlzgzg__ GHC.Base.op_zlzlzgzg____ GHC.Base.op_zlztzg____
+     GHC.Base.op_zsze__ GHC.Base.op_zsze____ GHC.Base.op_ztzg____ GHC.Base.pure
      GHC.Base.pure__ GHC.Base.return___ GHC.Num.Int GHC.Num.Num GHC.Num.fromInteger
      GHC.Prim.coerce
 *)
diff --git a/base/Data/Functor/Product.v b/base/Data/Functor/Product.v
index 4f14ffeb..2f9ded24 100644
--- a/base/Data/Functor/Product.v
+++ b/base/Data/Functor/Product.v
@@ -34,6 +34,15 @@ Arguments Pair {_} {_} {_} {_} _ _.
 
 (* Converted value declarations: *)
 
+(* Skipping all instances of class `Data.Data.Data', including
+   `Data.Functor.Product.Data__Product' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic', including
+   `Data.Functor.Product.Generic__Product' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic1', including
+   `Data.Functor.Product.Generic1__Product__5' *)
+
 #[local] Definition Eq1__Product_liftEq {inst_f : Type -> Type} {inst_g
    : Type -> Type} `{Data.Functor.Classes.Eq1 inst_f} `{Data.Functor.Classes.Eq1
   inst_g}
diff --git a/base/Data/Functor/Sum.v b/base/Data/Functor/Sum.v
index 3d4f90c2..270944ec 100644
--- a/base/Data/Functor/Sum.v
+++ b/base/Data/Functor/Sum.v
@@ -36,6 +36,15 @@ Arguments InR {_} {_} {_} {_} _.
 
 (* Converted value declarations: *)
 
+(* Skipping all instances of class `Data.Data.Data', including
+   `Data.Functor.Sum.Data__Sum' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic', including
+   `Data.Functor.Sum.Generic__Sum' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic1', including
+   `Data.Functor.Sum.Generic1__Sum__5' *)
+
 #[local] Definition Eq1__Sum_liftEq {inst_f : Type -> Type} {inst_g
    : Type -> Type} `{Data.Functor.Classes.Eq1 inst_f} `{Data.Functor.Classes.Eq1
   inst_g}
diff --git a/base/Data/Monoid.v b/base/Data/Monoid.v
index 32729e7c..98ce5019 100644
--- a/base/Data/Monoid.v
+++ b/base/Data/Monoid.v
@@ -12,7 +12,9 @@ Require Coq.Program.Wf.
 
 (* Converted imports: *)
 
+Require Control.Monad.Fail.
 Require GHC.Base.
+Require GHC.Prim.
 Require HsToCoq.Unpeel.
 Import GHC.Base.Notations.
 
@@ -22,14 +24,14 @@ Inductive Last a : Type := | Mk_Last (getLast : option a) : Last a.
 
 Inductive First a : Type := | Mk_First (getFirst : option a) : First a.
 
-Inductive Ap (f : Type -> Type) (a : Type) : Type :=
+Inductive Ap {k : Type} (f : k -> Type) (a : k) : Type :=
   | Mk_Ap (getAp : f a) : Ap f a.
 
 Arguments Mk_Last {_} _.
 
 Arguments Mk_First {_} _.
 
-Arguments Mk_Ap {_} {_} _.
+Arguments Mk_Ap {_} {_} {_} _.
 
 #[global] Definition getLast {a} (arg_0__ : Last a) :=
   let 'Mk_Last getLast := arg_0__ in
@@ -39,12 +41,459 @@ Arguments Mk_Ap {_} {_} _.
   let 'Mk_First getFirst := arg_0__ in
   getFirst.
 
-#[global] Definition getAp {f : Type -> Type} {a : Type} (arg_0__ : Ap f a) :=
+#[global] Definition getAp {k : Type} {f : k -> Type} {a : k} (arg_0__
+    : Ap f a) :=
   let 'Mk_Ap getAp := arg_0__ in
   getAp.
 
 (* Converted value declarations: *)
 
+(* Skipping all instances of class `GHC.Base.Alternative', including
+   `Data.Monoid.Alternative__Ap' *)
+
+Instance Unpeel_Ap (k : Type) (f : k -> Type) (a : k)
+   : HsToCoq.Unpeel.Unpeel (Ap f a) (f a) :=
+  HsToCoq.Unpeel.Build_Unpeel _ _ getAp Mk_Ap.
+
+#[local] Definition Applicative__Ap_liftA2 {inst_f : Type -> Type}
+  `{GHC.Base.Applicative inst_f}
+   : forall {a : Type},
+     forall {b : Type},
+     forall {c : Type}, (a -> b -> c) -> Ap inst_f a -> Ap inst_f b -> Ap inst_f c :=
+  fun {a : Type} {b : Type} {c : Type} => GHC.Prim.coerce (GHC.Base.liftA2).
+
+#[local] Definition Applicative__Ap_op_zlztzg__ {inst_f : Type -> Type}
+  `{GHC.Base.Applicative inst_f}
+   : forall {a : Type},
+     forall {b : Type}, Ap inst_f (a -> b) -> Ap inst_f a -> Ap inst_f b :=
+  fun {a : Type} {b : Type} => GHC.Prim.coerce (_GHC.Base.<*>_).
+
+#[local] Definition Applicative__Ap_op_ztzg__ {inst_f : Type -> Type}
+  `{GHC.Base.Applicative inst_f}
+   : forall {a : Type},
+     forall {b : Type}, Ap inst_f a -> Ap inst_f b -> Ap inst_f b :=
+  fun {a : Type} {b : Type} => GHC.Prim.coerce (_GHC.Base.*>_).
+
+#[local] Definition Applicative__Ap_pure {inst_f : Type -> Type}
+  `{GHC.Base.Applicative inst_f}
+   : forall {a : Type}, a -> Ap inst_f a :=
+  fun {a : Type} => GHC.Prim.coerce (GHC.Base.pure).
+
+#[local] Definition Functor__Ap_fmap {inst_f : Type -> Type} `{GHC.Base.Functor
+  inst_f}
+   : forall {a : Type},
+     forall {b : Type}, (a -> b) -> Ap inst_f a -> Ap inst_f b :=
+  fun {a : Type} {b : Type} => GHC.Prim.coerce (GHC.Base.fmap).
+
+#[local] Definition Functor__Ap_op_zlzd__ {inst_f : Type -> Type}
+  `{GHC.Base.Functor inst_f}
+   : forall {a : Type}, forall {b : Type}, a -> Ap inst_f b -> Ap inst_f a :=
+  fun {a : Type} {b : Type} => GHC.Prim.coerce (_GHC.Base.<$_).
+
+#[global]
+Program Instance Functor__Ap {f : Type -> Type} `{GHC.Base.Functor f}
+   : GHC.Base.Functor (Ap f) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.fmap__ := fun {a : Type} {b : Type} => Functor__Ap_fmap ;
+           GHC.Base.op_zlzd____ := fun {a : Type} {b : Type} => Functor__Ap_op_zlzd__ |}.
+
+#[global]
+Program Instance Applicative__Ap {f : Type -> Type} `{GHC.Base.Applicative f}
+   : GHC.Base.Applicative (Ap f) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.liftA2__ := fun {a : Type} {b : Type} {c : Type} =>
+             Applicative__Ap_liftA2 ;
+           GHC.Base.op_zlztzg____ := fun {a : Type} {b : Type} =>
+             Applicative__Ap_op_zlztzg__ ;
+           GHC.Base.op_ztzg____ := fun {a : Type} {b : Type} => Applicative__Ap_op_ztzg__ ;
+           GHC.Base.pure__ := fun {a : Type} => Applicative__Ap_pure |}.
+
+(* Skipping all instances of class `GHC.Enum.Enum', including
+   `Data.Monoid.Enum__Ap' *)
+
+#[local] Definition Eq___Ap_op_zeze__ {inst_k : Type} {inst_f : inst_k -> Type}
+  {inst_a : inst_k} `{GHC.Base.Eq_ (inst_f inst_a)}
+   : Ap inst_f inst_a -> Ap inst_f inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.==_).
+
+#[local] Definition Eq___Ap_op_zsze__ {inst_k : Type} {inst_f : inst_k -> Type}
+  {inst_a : inst_k} `{GHC.Base.Eq_ (inst_f inst_a)}
+   : Ap inst_f inst_a -> Ap inst_f inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base./=_).
+
+#[global]
+Program Instance Eq___Ap {k : Type} {f : k -> Type} {a : k} `{GHC.Base.Eq_ (f
+                                                                            a)}
+   : GHC.Base.Eq_ (Ap f a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zeze____ := Eq___Ap_op_zeze__ ;
+           GHC.Base.op_zsze____ := Eq___Ap_op_zsze__ |}.
+
+(* Skipping all instances of class `GHC.Generics.Generic', including
+   `Data.Monoid.Generic__Ap' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic1', including
+   `Data.Monoid.Generic1__Ap__5' *)
+
+#[local] Definition Monad__Ap_op_zgzg__ {inst_f : Type -> Type} `{GHC.Base.Monad
+  inst_f}
+   : forall {a : Type},
+     forall {b : Type}, Ap inst_f a -> Ap inst_f b -> Ap inst_f b :=
+  fun {a : Type} {b : Type} => GHC.Prim.coerce (_GHC.Base.>>_).
+
+#[local] Definition Monad__Ap_op_zgzgze__ {inst_f : Type -> Type}
+  `{GHC.Base.Monad inst_f}
+   : forall {a : Type},
+     forall {b : Type}, Ap inst_f a -> (a -> Ap inst_f b) -> Ap inst_f b :=
+  fun {a : Type} {b : Type} => GHC.Prim.coerce (_GHC.Base.>>=_).
+
+#[local] Definition Monad__Ap_return_ {inst_f : Type -> Type} `{GHC.Base.Monad
+  inst_f}
+   : forall {a : Type}, a -> Ap inst_f a :=
+  fun {a : Type} => GHC.Prim.coerce (GHC.Base.return_).
+
+#[global]
+Program Instance Monad__Ap {f : Type -> Type} `{GHC.Base.Monad f}
+   : GHC.Base.Monad (Ap f) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zgzg____ := fun {a : Type} {b : Type} =>
+             Monad__Ap_op_zgzg__ ;
+           GHC.Base.op_zgzgze____ := fun {a : Type} {b : Type} => Monad__Ap_op_zgzgze__ ;
+           GHC.Base.return___ := fun {a : Type} => Monad__Ap_return_ |}.
+
+#[local] Definition MonadFail__Ap_fail {inst_f : Type -> Type}
+  `{Control.Monad.Fail.MonadFail inst_f}
+   : forall {a : Type}, GHC.Base.String -> Ap inst_f a :=
+  fun {a : Type} => GHC.Prim.coerce (Control.Monad.Fail.fail).
+
+#[global]
+Program Instance MonadFail__Ap {f : Type -> Type} `{Control.Monad.Fail.MonadFail
+  f}
+   : Control.Monad.Fail.MonadFail (Ap f) :=
+  fun _ k__ =>
+    k__ {| Control.Monad.Fail.fail__ := fun {a : Type} => MonadFail__Ap_fail |}.
+
+(* Skipping all instances of class `GHC.Base.MonadPlus', including
+   `Data.Monoid.MonadPlus__Ap' *)
+
+#[local] Definition Ord__Ap_op_zl__ {inst_k : Type} {inst_f : inst_k -> Type}
+  {inst_a : inst_k} `{GHC.Base.Ord (inst_f inst_a)}
+   : Ap inst_f inst_a -> Ap inst_f inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<_).
+
+#[local] Definition Ord__Ap_op_zlze__ {inst_k : Type} {inst_f : inst_k -> Type}
+  {inst_a : inst_k} `{GHC.Base.Ord (inst_f inst_a)}
+   : Ap inst_f inst_a -> Ap inst_f inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<=_).
+
+#[local] Definition Ord__Ap_op_zg__ {inst_k : Type} {inst_f : inst_k -> Type}
+  {inst_a : inst_k} `{GHC.Base.Ord (inst_f inst_a)}
+   : Ap inst_f inst_a -> Ap inst_f inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>_).
+
+#[local] Definition Ord__Ap_op_zgze__ {inst_k : Type} {inst_f : inst_k -> Type}
+  {inst_a : inst_k} `{GHC.Base.Ord (inst_f inst_a)}
+   : Ap inst_f inst_a -> Ap inst_f inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>=_).
+
+#[local] Definition Ord__Ap_compare {inst_k : Type} {inst_f : inst_k -> Type}
+  {inst_a : inst_k} `{GHC.Base.Ord (inst_f inst_a)}
+   : Ap inst_f inst_a -> Ap inst_f inst_a -> comparison :=
+  GHC.Prim.coerce (GHC.Base.compare).
+
+#[local] Definition Ord__Ap_max {inst_k : Type} {inst_f : inst_k -> Type}
+  {inst_a : inst_k} `{GHC.Base.Ord (inst_f inst_a)}
+   : Ap inst_f inst_a -> Ap inst_f inst_a -> Ap inst_f inst_a :=
+  GHC.Prim.coerce (GHC.Base.max).
+
+#[local] Definition Ord__Ap_min {inst_k : Type} {inst_f : inst_k -> Type}
+  {inst_a : inst_k} `{GHC.Base.Ord (inst_f inst_a)}
+   : Ap inst_f inst_a -> Ap inst_f inst_a -> Ap inst_f inst_a :=
+  GHC.Prim.coerce (GHC.Base.min).
+
+#[global]
+Program Instance Ord__Ap {k : Type} {f : k -> Type} {a : k} `{GHC.Base.Ord (f
+                                                                            a)}
+   : GHC.Base.Ord (Ap f a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zl____ := Ord__Ap_op_zl__ ;
+           GHC.Base.op_zlze____ := Ord__Ap_op_zlze__ ;
+           GHC.Base.op_zg____ := Ord__Ap_op_zg__ ;
+           GHC.Base.op_zgze____ := Ord__Ap_op_zgze__ ;
+           GHC.Base.compare__ := Ord__Ap_compare ;
+           GHC.Base.max__ := Ord__Ap_max ;
+           GHC.Base.min__ := Ord__Ap_min |}.
+
+(* Skipping all instances of class `GHC.Read.Read', including
+   `Data.Monoid.Read__Ap' *)
+
+(* Skipping all instances of class `GHC.Show.Show', including
+   `Data.Monoid.Show__Ap' *)
+
+Instance Unpeel_Last a : HsToCoq.Unpeel.Unpeel (Last a) (option a) :=
+  HsToCoq.Unpeel.Build_Unpeel _ _ getLast Mk_Last.
+
+#[local] Definition Eq___Last_op_zeze__ {inst_a : Type} `{GHC.Base.Eq_ inst_a}
+   : Last inst_a -> Last inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.==_).
+
+#[local] Definition Eq___Last_op_zsze__ {inst_a : Type} `{GHC.Base.Eq_ inst_a}
+   : Last inst_a -> Last inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base./=_).
+
+#[global]
+Program Instance Eq___Last {a : Type} `{GHC.Base.Eq_ a}
+   : GHC.Base.Eq_ (Last a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zeze____ := Eq___Last_op_zeze__ ;
+           GHC.Base.op_zsze____ := Eq___Last_op_zsze__ |}.
+
+#[local] Definition Ord__Last_op_zl__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Last inst_a -> Last inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<_).
+
+#[local] Definition Ord__Last_op_zlze__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Last inst_a -> Last inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<=_).
+
+#[local] Definition Ord__Last_op_zg__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Last inst_a -> Last inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>_).
+
+#[local] Definition Ord__Last_op_zgze__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Last inst_a -> Last inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>=_).
+
+#[local] Definition Ord__Last_compare {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Last inst_a -> Last inst_a -> comparison :=
+  GHC.Prim.coerce (GHC.Base.compare).
+
+#[local] Definition Ord__Last_max {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Last inst_a -> Last inst_a -> Last inst_a :=
+  GHC.Prim.coerce (GHC.Base.max).
+
+#[local] Definition Ord__Last_min {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Last inst_a -> Last inst_a -> Last inst_a :=
+  GHC.Prim.coerce (GHC.Base.min).
+
+#[global]
+Program Instance Ord__Last {a : Type} `{GHC.Base.Ord a}
+   : GHC.Base.Ord (Last a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zl____ := Ord__Last_op_zl__ ;
+           GHC.Base.op_zlze____ := Ord__Last_op_zlze__ ;
+           GHC.Base.op_zg____ := Ord__Last_op_zg__ ;
+           GHC.Base.op_zgze____ := Ord__Last_op_zgze__ ;
+           GHC.Base.compare__ := Ord__Last_compare ;
+           GHC.Base.max__ := Ord__Last_max ;
+           GHC.Base.min__ := Ord__Last_min |}.
+
+(* Skipping all instances of class `GHC.Read.Read', including
+   `Data.Monoid.Read__Last' *)
+
+(* Skipping all instances of class `GHC.Show.Show', including
+   `Data.Monoid.Show__Last' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic', including
+   `Data.Monoid.Generic__Last' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic1', including
+   `Data.Monoid.Generic1__TYPE__Last__LiftedRep' *)
+
+#[local] Definition Functor__Last_fmap
+   : forall {a : Type}, forall {b : Type}, (a -> b) -> Last a -> Last b :=
+  fun {a : Type} {b : Type} => GHC.Prim.coerce (GHC.Base.fmap).
+
+#[local] Definition Functor__Last_op_zlzd__
+   : forall {a : Type}, forall {b : Type}, a -> Last b -> Last a :=
+  fun {a : Type} {b : Type} => GHC.Prim.coerce (_GHC.Base.<$_).
+
+#[global]
+Program Instance Functor__Last : GHC.Base.Functor Last :=
+  fun _ k__ =>
+    k__ {| GHC.Base.fmap__ := fun {a : Type} {b : Type} => Functor__Last_fmap ;
+           GHC.Base.op_zlzd____ := fun {a : Type} {b : Type} => Functor__Last_op_zlzd__ |}.
+
+#[local] Definition Applicative__Last_liftA2
+   : forall {a : Type},
+     forall {b : Type},
+     forall {c : Type}, (a -> b -> c) -> Last a -> Last b -> Last c :=
+  fun {a : Type} {b : Type} {c : Type} => GHC.Prim.coerce (GHC.Base.liftA2).
+
+#[local] Definition Applicative__Last_op_zlztzg__
+   : forall {a : Type}, forall {b : Type}, Last (a -> b) -> Last a -> Last b :=
+  fun {a : Type} {b : Type} => GHC.Prim.coerce (_GHC.Base.<*>_).
+
+#[local] Definition Applicative__Last_op_ztzg__
+   : forall {a : Type}, forall {b : Type}, Last a -> Last b -> Last b :=
+  fun {a : Type} {b : Type} => GHC.Prim.coerce (_GHC.Base.*>_).
+
+#[local] Definition Applicative__Last_pure : forall {a : Type}, a -> Last a :=
+  fun {a : Type} => GHC.Prim.coerce (GHC.Base.pure).
+
+#[global]
+Program Instance Applicative__Last : GHC.Base.Applicative Last :=
+  fun _ k__ =>
+    k__ {| GHC.Base.liftA2__ := fun {a : Type} {b : Type} {c : Type} =>
+             Applicative__Last_liftA2 ;
+           GHC.Base.op_zlztzg____ := fun {a : Type} {b : Type} =>
+             Applicative__Last_op_zlztzg__ ;
+           GHC.Base.op_ztzg____ := fun {a : Type} {b : Type} =>
+             Applicative__Last_op_ztzg__ ;
+           GHC.Base.pure__ := fun {a : Type} => Applicative__Last_pure |}.
+
+#[local] Definition Monad__Last_op_zgzg__
+   : forall {a : Type}, forall {b : Type}, Last a -> Last b -> Last b :=
+  fun {a : Type} {b : Type} => GHC.Prim.coerce (_GHC.Base.>>_).
+
+#[local] Definition Monad__Last_op_zgzgze__
+   : forall {a : Type}, forall {b : Type}, Last a -> (a -> Last b) -> Last b :=
+  fun {a : Type} {b : Type} => GHC.Prim.coerce (_GHC.Base.>>=_).
+
+#[local] Definition Monad__Last_return_ : forall {a : Type}, a -> Last a :=
+  fun {a : Type} => GHC.Prim.coerce (GHC.Base.return_).
+
+#[global]
+Program Instance Monad__Last : GHC.Base.Monad Last :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zgzg____ := fun {a : Type} {b : Type} =>
+             Monad__Last_op_zgzg__ ;
+           GHC.Base.op_zgzgze____ := fun {a : Type} {b : Type} => Monad__Last_op_zgzgze__ ;
+           GHC.Base.return___ := fun {a : Type} => Monad__Last_return_ |}.
+
+Instance Unpeel_First a : HsToCoq.Unpeel.Unpeel (First a) (option a) :=
+  HsToCoq.Unpeel.Build_Unpeel _ _ getFirst Mk_First.
+
+#[local] Definition Eq___First_op_zeze__ {inst_a : Type} `{GHC.Base.Eq_ inst_a}
+   : First inst_a -> First inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.==_).
+
+#[local] Definition Eq___First_op_zsze__ {inst_a : Type} `{GHC.Base.Eq_ inst_a}
+   : First inst_a -> First inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base./=_).
+
+#[global]
+Program Instance Eq___First {a : Type} `{GHC.Base.Eq_ a}
+   : GHC.Base.Eq_ (First a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zeze____ := Eq___First_op_zeze__ ;
+           GHC.Base.op_zsze____ := Eq___First_op_zsze__ |}.
+
+#[local] Definition Ord__First_op_zl__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : First inst_a -> First inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<_).
+
+#[local] Definition Ord__First_op_zlze__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : First inst_a -> First inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<=_).
+
+#[local] Definition Ord__First_op_zg__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : First inst_a -> First inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>_).
+
+#[local] Definition Ord__First_op_zgze__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : First inst_a -> First inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>=_).
+
+#[local] Definition Ord__First_compare {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : First inst_a -> First inst_a -> comparison :=
+  GHC.Prim.coerce (GHC.Base.compare).
+
+#[local] Definition Ord__First_max {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : First inst_a -> First inst_a -> First inst_a :=
+  GHC.Prim.coerce (GHC.Base.max).
+
+#[local] Definition Ord__First_min {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : First inst_a -> First inst_a -> First inst_a :=
+  GHC.Prim.coerce (GHC.Base.min).
+
+#[global]
+Program Instance Ord__First {a : Type} `{GHC.Base.Ord a}
+   : GHC.Base.Ord (First a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zl____ := Ord__First_op_zl__ ;
+           GHC.Base.op_zlze____ := Ord__First_op_zlze__ ;
+           GHC.Base.op_zg____ := Ord__First_op_zg__ ;
+           GHC.Base.op_zgze____ := Ord__First_op_zgze__ ;
+           GHC.Base.compare__ := Ord__First_compare ;
+           GHC.Base.max__ := Ord__First_max ;
+           GHC.Base.min__ := Ord__First_min |}.
+
+(* Skipping all instances of class `GHC.Read.Read', including
+   `Data.Monoid.Read__First' *)
+
+(* Skipping all instances of class `GHC.Show.Show', including
+   `Data.Monoid.Show__First' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic', including
+   `Data.Monoid.Generic__First' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic1', including
+   `Data.Monoid.Generic1__TYPE__First__LiftedRep' *)
+
+#[local] Definition Functor__First_fmap
+   : forall {a : Type}, forall {b : Type}, (a -> b) -> First a -> First b :=
+  fun {a : Type} {b : Type} => GHC.Prim.coerce (GHC.Base.fmap).
+
+#[local] Definition Functor__First_op_zlzd__
+   : forall {a : Type}, forall {b : Type}, a -> First b -> First a :=
+  fun {a : Type} {b : Type} => GHC.Prim.coerce (_GHC.Base.<$_).
+
+#[global]
+Program Instance Functor__First : GHC.Base.Functor First :=
+  fun _ k__ =>
+    k__ {| GHC.Base.fmap__ := fun {a : Type} {b : Type} => Functor__First_fmap ;
+           GHC.Base.op_zlzd____ := fun {a : Type} {b : Type} =>
+             Functor__First_op_zlzd__ |}.
+
+#[local] Definition Applicative__First_liftA2
+   : forall {a : Type},
+     forall {b : Type},
+     forall {c : Type}, (a -> b -> c) -> First a -> First b -> First c :=
+  fun {a : Type} {b : Type} {c : Type} => GHC.Prim.coerce (GHC.Base.liftA2).
+
+#[local] Definition Applicative__First_op_zlztzg__
+   : forall {a : Type}, forall {b : Type}, First (a -> b) -> First a -> First b :=
+  fun {a : Type} {b : Type} => GHC.Prim.coerce (_GHC.Base.<*>_).
+
+#[local] Definition Applicative__First_op_ztzg__
+   : forall {a : Type}, forall {b : Type}, First a -> First b -> First b :=
+  fun {a : Type} {b : Type} => GHC.Prim.coerce (_GHC.Base.*>_).
+
+#[local] Definition Applicative__First_pure : forall {a : Type}, a -> First a :=
+  fun {a : Type} => GHC.Prim.coerce (GHC.Base.pure).
+
+#[global]
+Program Instance Applicative__First : GHC.Base.Applicative First :=
+  fun _ k__ =>
+    k__ {| GHC.Base.liftA2__ := fun {a : Type} {b : Type} {c : Type} =>
+             Applicative__First_liftA2 ;
+           GHC.Base.op_zlztzg____ := fun {a : Type} {b : Type} =>
+             Applicative__First_op_zlztzg__ ;
+           GHC.Base.op_ztzg____ := fun {a : Type} {b : Type} =>
+             Applicative__First_op_ztzg__ ;
+           GHC.Base.pure__ := fun {a : Type} => Applicative__First_pure |}.
+
+#[local] Definition Monad__First_op_zgzg__
+   : forall {a : Type}, forall {b : Type}, First a -> First b -> First b :=
+  fun {a : Type} {b : Type} => GHC.Prim.coerce (_GHC.Base.>>_).
+
+#[local] Definition Monad__First_op_zgzgze__
+   : forall {a : Type}, forall {b : Type}, First a -> (a -> First b) -> First b :=
+  fun {a : Type} {b : Type} => GHC.Prim.coerce (_GHC.Base.>>=_).
+
+#[local] Definition Monad__First_return_ : forall {a : Type}, a -> First a :=
+  fun {a : Type} => GHC.Prim.coerce (GHC.Base.return_).
+
+#[global]
+Program Instance Monad__First : GHC.Base.Monad First :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zgzg____ := fun {a : Type} {b : Type} =>
+             Monad__First_op_zgzg__ ;
+           GHC.Base.op_zgzgze____ := fun {a : Type} {b : Type} =>
+             Monad__First_op_zgzgze__ ;
+           GHC.Base.return___ := fun {a : Type} => Monad__First_return_ |}.
+
 #[local] Definition Semigroup__First_op_zlzlzgzg__ {inst_a : Type}
    : First inst_a -> First inst_a -> First inst_a :=
   fun arg_0__ arg_1__ =>
@@ -151,16 +600,21 @@ Program Instance Monoid__Ap {f : Type -> Type} {a : Type} `{GHC.Base.Applicative
 (* Skipping all instances of class `GHC.Num.Num', including
    `Data.Monoid.Num__Ap' *)
 
-Instance Unpeel_Last a : HsToCoq.Unpeel.Unpeel (Last a) (option a) :=
-  HsToCoq.Unpeel.Build_Unpeel _ _ getLast Mk_Last.
-
-Instance Unpeel_First a : HsToCoq.Unpeel.Unpeel (First a) (option a) :=
-  HsToCoq.Unpeel.Build_Unpeel _ _ getFirst Mk_First.
-
 (* External variables:
-     None Type list option GHC.Base.Applicative GHC.Base.Monoid GHC.Base.Semigroup
-     GHC.Base.foldr GHC.Base.liftA2 GHC.Base.mappend__ GHC.Base.mconcat__
-     GHC.Base.mempty GHC.Base.mempty__ GHC.Base.op_zlzlzgzg__
-     GHC.Base.op_zlzlzgzg____ GHC.Base.pure HsToCoq.Unpeel.Build_Unpeel
+     None Type bool comparison list option Control.Monad.Fail.MonadFail
+     Control.Monad.Fail.fail Control.Monad.Fail.fail__ GHC.Base.Applicative
+     GHC.Base.Eq_ GHC.Base.Functor GHC.Base.Monad GHC.Base.Monoid GHC.Base.Ord
+     GHC.Base.Semigroup GHC.Base.String GHC.Base.compare GHC.Base.compare__
+     GHC.Base.fmap GHC.Base.fmap__ GHC.Base.foldr GHC.Base.liftA2 GHC.Base.liftA2__
+     GHC.Base.mappend__ GHC.Base.max GHC.Base.max__ GHC.Base.mconcat__
+     GHC.Base.mempty GHC.Base.mempty__ GHC.Base.min GHC.Base.min__ GHC.Base.op_zeze__
+     GHC.Base.op_zeze____ GHC.Base.op_zg__ GHC.Base.op_zg____ GHC.Base.op_zgze__
+     GHC.Base.op_zgze____ GHC.Base.op_zgzg__ GHC.Base.op_zgzg____
+     GHC.Base.op_zgzgze__ GHC.Base.op_zgzgze____ GHC.Base.op_zl__ GHC.Base.op_zl____
+     GHC.Base.op_zlzd__ GHC.Base.op_zlzd____ GHC.Base.op_zlze__ GHC.Base.op_zlze____
+     GHC.Base.op_zlzlzgzg__ GHC.Base.op_zlzlzgzg____ GHC.Base.op_zlztzg__
+     GHC.Base.op_zlztzg____ GHC.Base.op_zsze__ GHC.Base.op_zsze____
+     GHC.Base.op_ztzg__ GHC.Base.op_ztzg____ GHC.Base.pure GHC.Base.pure__
+     GHC.Base.return_ GHC.Base.return___ GHC.Prim.coerce HsToCoq.Unpeel.Build_Unpeel
      HsToCoq.Unpeel.Unpeel
 *)
diff --git a/base/Data/OldList.v b/base/Data/OldList.v
index 31137541..627ab7c1 100644
--- a/base/Data/OldList.v
+++ b/base/Data/OldList.v
@@ -39,7 +39,7 @@ Arguments Mk_SnocBuilder {_} _ _ _.
 Require Import GHC.Char.
 Require GHC.Unicode.
 Require Coq.Lists.List.
-Require Import Omega.
+Require Import Lia.
 Import Ascii.AsciiSyntax.
 Import String.StringSyntax.
 
@@ -118,13 +118,13 @@ Lemma mergePairs_length : forall n, forall a cmp (xs : list (list a)) x y,
 induction n. intros; simpl. destruct xs; inversion H. simpl. auto.
 intros.
 destruct xs.
-simpl in *. omega.
+simpl in *. lia.
 destruct xs.
-simpl in *. omega.
+simpl in *. lia.
 assert (L : le (length xs) n).
-simpl in H. omega.
+simpl in H. lia.
 specialize (IHn a cmp xs l l0 L).
-simpl in *. omega.
+simpl in *. lia.
 Qed.
 
 Program Fixpoint mergeAll {a0} (cmp: a0 -> a0 -> comparison)
@@ -138,10 +138,10 @@ Next Obligation.
 simpl.
 destruct xs. simpl. auto.
 destruct xs. simpl. auto.
-apply lt_n_S.
+apply Nat.succ_lt_mono.
 pose (MP := mergePairs_length (length xs) a0 cmp xs l l0 ltac:(auto)). clearbody MP.
 simpl in *.
-omega.
+lia.
 Defined.
 
 Definition sortBy {a} (cmp : a -> a -> comparison) (xs : list a): list a :=
@@ -170,7 +170,7 @@ Proof.
   + intros p s' H. simpl in *.
     destruct (p a) eqn:Hp.
     pose (K := IHs p s' H). clearbody K.
-    omega.
+    lia.
     inversion H. subst.
     auto.
 Qed.
@@ -209,7 +209,7 @@ Next Obligation.
   inversion Heq_anonymous. subst.
   symmetry in B.
   pose (h2 := break_length B).
-  omega.
+  lia.
 Defined.
 
 Program Fixpoint lines (s : GHC.Base.String) { measure (length s) }
@@ -222,7 +222,7 @@ Program Fixpoint lines (s : GHC.Base.String) { measure (length s) }
          pair l (match s' with | nil => nil | cons _ s'' => lines s'' end)).
 Next Obligation.
   pose (h0 := break_length Heq_anonymous). clearbody h0. simpl in h0.
-  omega.
+  lia.
 Defined.
 
 (* Converted value declarations: *)
diff --git a/base/Data/Ord.v b/base/Data/Ord.v
index 77f8674c..974d1afa 100644
--- a/base/Data/Ord.v
+++ b/base/Data/Ord.v
@@ -27,23 +27,97 @@ Arguments Mk_Down {_} _.
   let 'Mk_Down getDown := arg_0__ in
   getDown.
 
-(* Midamble *)
+(* Converted value declarations: *)
+
+Instance Unpeel_Down a : HsToCoq.Unpeel.Unpeel (Down a) a :=
+  HsToCoq.Unpeel.Build_Unpeel _ _ (fun '(Mk_Down x) => x) Mk_Down.
 
 #[local] Definition Eq___Down_op_zeze__ {inst_a : Type} `{GHC.Base.Eq_ inst_a}
    : Down inst_a -> Down inst_a -> bool :=
-  GHC.Prim.coerce _GHC.Base.==_.
+  GHC.Prim.coerce (_GHC.Base.==_).
 
 #[local] Definition Eq___Down_op_zsze__ {inst_a : Type} `{GHC.Base.Eq_ inst_a}
    : Down inst_a -> Down inst_a -> bool :=
-  GHC.Prim.coerce _GHC.Base./=_.
+  GHC.Prim.coerce (_GHC.Base./=_).
 
-#[global] Program Instance Eq___Down {a : Type} `{GHC.Base.Eq_ a}
+#[global]
+Program Instance Eq___Down {a : Type} `{GHC.Base.Eq_ a}
    : GHC.Base.Eq_ (Down a) :=
   fun _ k__ =>
     k__ {| GHC.Base.op_zeze____ := Eq___Down_op_zeze__ ;
            GHC.Base.op_zsze____ := Eq___Down_op_zsze__ |}.
 
-(* Converted value declarations: *)
+(* Skipping all instances of class `GHC.Num.Num', including
+   `Data.Ord.Num__Down' *)
+
+#[local] Definition Semigroup__Down_op_zlzlzgzg__ {inst_a : Type}
+  `{GHC.Base.Semigroup inst_a}
+   : Down inst_a -> Down inst_a -> Down inst_a :=
+  GHC.Prim.coerce (_GHC.Base.<<>>_).
+
+#[global]
+Program Instance Semigroup__Down {a : Type} `{GHC.Base.Semigroup a}
+   : GHC.Base.Semigroup (Down a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zlzlzgzg____ := Semigroup__Down_op_zlzlzgzg__ |}.
+
+#[local] Definition Monoid__Down_mappend {inst_a : Type} `{GHC.Base.Monoid
+  inst_a}
+   : Down inst_a -> Down inst_a -> Down inst_a :=
+  GHC.Prim.coerce (GHC.Base.mappend).
+
+#[local] Definition Monoid__Down_mconcat {inst_a : Type} `{GHC.Base.Monoid
+  inst_a}
+   : list (Down inst_a) -> Down inst_a :=
+  GHC.Prim.coerce (GHC.Base.mconcat).
+
+#[local] Definition Monoid__Down_mempty {inst_a : Type} `{GHC.Base.Monoid
+  inst_a}
+   : Down inst_a :=
+  GHC.Prim.coerce (GHC.Base.mempty).
+
+#[global]
+Program Instance Monoid__Down {a : Type} `{GHC.Base.Monoid a}
+   : GHC.Base.Monoid (Down a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.mappend__ := Monoid__Down_mappend ;
+           GHC.Base.mconcat__ := Monoid__Down_mconcat ;
+           GHC.Base.mempty__ := Monoid__Down_mempty |}.
+
+(* Skipping all instances of class `Data.Bits.Bits', including
+   `Data.Ord.Bits__Down' *)
+
+(* Skipping all instances of class `GHC.Enum.Bounded', including
+   `Data.Ord.Bounded__Down' *)
+
+(* Skipping all instances of class `GHC.Enum.Enum', including
+   `Data.Ord.Enum__Down' *)
+
+(* Skipping all instances of class `Data.Bits.FiniteBits', including
+   `Data.Ord.FiniteBits__Down' *)
+
+(* Skipping all instances of class `GHC.Float.Floating', including
+   `Data.Ord.Floating__Down' *)
+
+(* Skipping all instances of class `GHC.Real.Fractional', including
+   `Data.Ord.Fractional__Down' *)
+
+(* Skipping all instances of class `GHC.Real.Integral', including
+   `Data.Ord.Integral__Down' *)
+
+(* Skipping all instances of class `GHC.Ix.Ix', including `Data.Ord.Ix__Down' *)
+
+(* Skipping all instances of class `GHC.Real.Real', including
+   `Data.Ord.Real__Down' *)
+
+(* Skipping all instances of class `GHC.Real.RealFrac', including
+   `Data.Ord.RealFrac__Down' *)
+
+(* Skipping all instances of class `GHC.Float.RealFloat', including
+   `Data.Ord.RealFloat__Down' *)
+
+(* Skipping all instances of class `Foreign.Storable.Storable', including
+   `Data.Ord.Storable__Down' *)
 
 (* Skipping all instances of class `GHC.Read.Read', including
    `Data.Ord.Read__Down' *)
@@ -163,17 +237,18 @@ Program Instance Monad__Down : GHC.Base.Monad Down :=
    : (b -> a) -> b -> b -> comparison :=
   fun p x y => GHC.Base.compare (p x) (p y).
 
-Instance Unpeel_Down a : HsToCoq.Unpeel.Unpeel (Down a) a :=
-  HsToCoq.Unpeel.Build_Unpeel _ _ (fun '(Mk_Down x) => x) Mk_Down.
-
 (* External variables:
-     Gt Lt Type bool comparison GHC.Base.Applicative GHC.Base.Functor GHC.Base.Monad
-     GHC.Base.Ord GHC.Base.compare GHC.Base.compare__ GHC.Base.const GHC.Base.fmap
-     GHC.Base.fmap__ GHC.Base.id GHC.Base.liftA2__ GHC.Base.max__ GHC.Base.min__
-     GHC.Base.op_z2218U__ GHC.Base.op_zeze__ GHC.Base.op_zg____ GHC.Base.op_zgze____
-     GHC.Base.op_zgzg____ GHC.Base.op_zgzgze____ GHC.Base.op_zl____
-     GHC.Base.op_zlzd__ GHC.Base.op_zlzd____ GHC.Base.op_zlze____
-     GHC.Base.op_zlztzg____ GHC.Base.op_zsze__ GHC.Base.op_ztzg____ GHC.Base.pure
-     GHC.Base.pure__ GHC.Base.return___ GHC.Prim.coerce HsToCoq.Unpeel.Build_Unpeel
+     Gt Lt Type bool comparison list GHC.Base.Applicative GHC.Base.Eq_
+     GHC.Base.Functor GHC.Base.Monad GHC.Base.Monoid GHC.Base.Ord GHC.Base.Semigroup
+     GHC.Base.compare GHC.Base.compare__ GHC.Base.const GHC.Base.fmap GHC.Base.fmap__
+     GHC.Base.id GHC.Base.liftA2__ GHC.Base.mappend GHC.Base.mappend__ GHC.Base.max__
+     GHC.Base.mconcat GHC.Base.mconcat__ GHC.Base.mempty GHC.Base.mempty__
+     GHC.Base.min__ GHC.Base.op_z2218U__ GHC.Base.op_zeze__ GHC.Base.op_zeze____
+     GHC.Base.op_zg____ GHC.Base.op_zgze____ GHC.Base.op_zgzg____
+     GHC.Base.op_zgzgze____ GHC.Base.op_zl____ GHC.Base.op_zlzd__
+     GHC.Base.op_zlzd____ GHC.Base.op_zlze____ GHC.Base.op_zlzlzgzg__
+     GHC.Base.op_zlzlzgzg____ GHC.Base.op_zlztzg____ GHC.Base.op_zsze__
+     GHC.Base.op_zsze____ GHC.Base.op_ztzg____ GHC.Base.pure GHC.Base.pure__
+     GHC.Base.return___ GHC.Prim.coerce HsToCoq.Unpeel.Build_Unpeel
      HsToCoq.Unpeel.Unpeel
 *)
diff --git a/base/Data/Proxy.v b/base/Data/Proxy.v
index ffecbd86..4f77ae28 100644
--- a/base/Data/Proxy.v
+++ b/base/Data/Proxy.v
@@ -31,6 +31,12 @@ Arguments Mk_KProxy {_}.
 
 (* Converted value declarations: *)
 
+(* Skipping all instances of class `GHC.Enum.Bounded', including
+   `Data.Proxy.Bounded__Proxy' *)
+
+(* Skipping all instances of class `GHC.Read.Read', including
+   `Data.Proxy.Read__Proxy' *)
+
 #[local] Definition Eq___Proxy_op_zeze__ {inst_k : Type} {inst_s : inst_k}
    : Proxy inst_s -> Proxy inst_s -> bool :=
   fun arg_0__ arg_1__ => true.
diff --git a/base/Data/Semigroup.v b/base/Data/Semigroup.v
index 33c1a2c0..2e7e3dff 100644
--- a/base/Data/Semigroup.v
+++ b/base/Data/Semigroup.v
@@ -149,6 +149,479 @@ Program Instance Semigroup__SLast {a} : GHC.Base.Semigroup (Last a) := fun _ k =
 
 (* Converted value declarations: *)
 
+Instance Unpeel_Option a : HsToCoq.Unpeel.Unpeel (Option a) (option a) :=
+  HsToCoq.Unpeel.Build_Unpeel _ _ getOption Mk_Option.
+
+#[local] Definition Eq___Option_op_zeze__ {inst_a : Type} `{GHC.Base.Eq_ inst_a}
+   : Option inst_a -> Option inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.==_).
+
+#[local] Definition Eq___Option_op_zsze__ {inst_a : Type} `{GHC.Base.Eq_ inst_a}
+   : Option inst_a -> Option inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base./=_).
+
+#[global]
+Program Instance Eq___Option {a : Type} `{GHC.Base.Eq_ a}
+   : GHC.Base.Eq_ (Option a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zeze____ := Eq___Option_op_zeze__ ;
+           GHC.Base.op_zsze____ := Eq___Option_op_zsze__ |}.
+
+#[local] Definition Ord__Option_op_zl__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Option inst_a -> Option inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<_).
+
+#[local] Definition Ord__Option_op_zlze__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Option inst_a -> Option inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<=_).
+
+#[local] Definition Ord__Option_op_zg__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Option inst_a -> Option inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>_).
+
+#[local] Definition Ord__Option_op_zgze__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Option inst_a -> Option inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>=_).
+
+#[local] Definition Ord__Option_compare {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Option inst_a -> Option inst_a -> comparison :=
+  GHC.Prim.coerce (GHC.Base.compare).
+
+#[local] Definition Ord__Option_max {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Option inst_a -> Option inst_a -> Option inst_a :=
+  GHC.Prim.coerce (GHC.Base.max).
+
+#[local] Definition Ord__Option_min {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Option inst_a -> Option inst_a -> Option inst_a :=
+  GHC.Prim.coerce (GHC.Base.min).
+
+#[global]
+Program Instance Ord__Option {a : Type} `{GHC.Base.Ord a}
+   : GHC.Base.Ord (Option a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zl____ := Ord__Option_op_zl__ ;
+           GHC.Base.op_zlze____ := Ord__Option_op_zlze__ ;
+           GHC.Base.op_zg____ := Ord__Option_op_zg__ ;
+           GHC.Base.op_zgze____ := Ord__Option_op_zgze__ ;
+           GHC.Base.compare__ := Ord__Option_compare ;
+           GHC.Base.max__ := Ord__Option_max ;
+           GHC.Base.min__ := Ord__Option_min |}.
+
+(* Skipping all instances of class `GHC.Show.Show', including
+   `Data.Semigroup.Show__Option' *)
+
+(* Skipping all instances of class `GHC.Read.Read', including
+   `Data.Semigroup.Read__Option' *)
+
+(* Skipping all instances of class `Data.Data.Data', including
+   `Data.Semigroup.Data__Option' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic', including
+   `Data.Semigroup.Generic__Option' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic1', including
+   `Data.Semigroup.Generic1__TYPE__Option__LiftedRep' *)
+
+(* Skipping all instances of class `GHC.Enum.Bounded', including
+   `Data.Semigroup.Bounded__WrappedMonoid' *)
+
+Instance Unpeel_WrappedMonoid a : HsToCoq.Unpeel.Unpeel (WrappedMonoid a) a :=
+  HsToCoq.Unpeel.Build_Unpeel _ _ unwrapMonoid WrapMonoid.
+
+#[local] Definition Eq___WrappedMonoid_op_zeze__ {inst_m : Type} `{GHC.Base.Eq_
+  inst_m}
+   : WrappedMonoid inst_m -> WrappedMonoid inst_m -> bool :=
+  GHC.Prim.coerce (_GHC.Base.==_).
+
+#[local] Definition Eq___WrappedMonoid_op_zsze__ {inst_m : Type} `{GHC.Base.Eq_
+  inst_m}
+   : WrappedMonoid inst_m -> WrappedMonoid inst_m -> bool :=
+  GHC.Prim.coerce (_GHC.Base./=_).
+
+#[global]
+Program Instance Eq___WrappedMonoid {m : Type} `{GHC.Base.Eq_ m}
+   : GHC.Base.Eq_ (WrappedMonoid m) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zeze____ := Eq___WrappedMonoid_op_zeze__ ;
+           GHC.Base.op_zsze____ := Eq___WrappedMonoid_op_zsze__ |}.
+
+#[local] Definition Ord__WrappedMonoid_op_zl__ {inst_m : Type} `{GHC.Base.Ord
+  inst_m}
+   : WrappedMonoid inst_m -> WrappedMonoid inst_m -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<_).
+
+#[local] Definition Ord__WrappedMonoid_op_zlze__ {inst_m : Type} `{GHC.Base.Ord
+  inst_m}
+   : WrappedMonoid inst_m -> WrappedMonoid inst_m -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<=_).
+
+#[local] Definition Ord__WrappedMonoid_op_zg__ {inst_m : Type} `{GHC.Base.Ord
+  inst_m}
+   : WrappedMonoid inst_m -> WrappedMonoid inst_m -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>_).
+
+#[local] Definition Ord__WrappedMonoid_op_zgze__ {inst_m : Type} `{GHC.Base.Ord
+  inst_m}
+   : WrappedMonoid inst_m -> WrappedMonoid inst_m -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>=_).
+
+#[local] Definition Ord__WrappedMonoid_compare {inst_m : Type} `{GHC.Base.Ord
+  inst_m}
+   : WrappedMonoid inst_m -> WrappedMonoid inst_m -> comparison :=
+  GHC.Prim.coerce (GHC.Base.compare).
+
+#[local] Definition Ord__WrappedMonoid_max {inst_m : Type} `{GHC.Base.Ord
+  inst_m}
+   : WrappedMonoid inst_m -> WrappedMonoid inst_m -> WrappedMonoid inst_m :=
+  GHC.Prim.coerce (GHC.Base.max).
+
+#[local] Definition Ord__WrappedMonoid_min {inst_m : Type} `{GHC.Base.Ord
+  inst_m}
+   : WrappedMonoid inst_m -> WrappedMonoid inst_m -> WrappedMonoid inst_m :=
+  GHC.Prim.coerce (GHC.Base.min).
+
+#[global]
+Program Instance Ord__WrappedMonoid {m : Type} `{GHC.Base.Ord m}
+   : GHC.Base.Ord (WrappedMonoid m) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zl____ := Ord__WrappedMonoid_op_zl__ ;
+           GHC.Base.op_zlze____ := Ord__WrappedMonoid_op_zlze__ ;
+           GHC.Base.op_zg____ := Ord__WrappedMonoid_op_zg__ ;
+           GHC.Base.op_zgze____ := Ord__WrappedMonoid_op_zgze__ ;
+           GHC.Base.compare__ := Ord__WrappedMonoid_compare ;
+           GHC.Base.max__ := Ord__WrappedMonoid_max ;
+           GHC.Base.min__ := Ord__WrappedMonoid_min |}.
+
+(* Skipping all instances of class `GHC.Show.Show', including
+   `Data.Semigroup.Show__WrappedMonoid' *)
+
+(* Skipping all instances of class `GHC.Read.Read', including
+   `Data.Semigroup.Read__WrappedMonoid' *)
+
+(* Skipping all instances of class `Data.Data.Data', including
+   `Data.Semigroup.Data__WrappedMonoid' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic', including
+   `Data.Semigroup.Generic__WrappedMonoid' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic1', including
+   `Data.Semigroup.Generic1__TYPE__WrappedMonoid__LiftedRep' *)
+
+(* Skipping all instances of class `GHC.Enum.Bounded', including
+   `Data.Semigroup.Bounded__Last' *)
+
+Instance Unpeel_Last a : HsToCoq.Unpeel.Unpeel (Last a) a :=
+  HsToCoq.Unpeel.Build_Unpeel _ _ getLast Mk_Last.
+
+#[local] Definition Eq___Last_op_zeze__ {inst_a : Type} `{GHC.Base.Eq_ inst_a}
+   : Last inst_a -> Last inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.==_).
+
+#[local] Definition Eq___Last_op_zsze__ {inst_a : Type} `{GHC.Base.Eq_ inst_a}
+   : Last inst_a -> Last inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base./=_).
+
+#[global]
+Program Instance Eq___Last {a : Type} `{GHC.Base.Eq_ a}
+   : GHC.Base.Eq_ (Last a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zeze____ := Eq___Last_op_zeze__ ;
+           GHC.Base.op_zsze____ := Eq___Last_op_zsze__ |}.
+
+#[local] Definition Ord__Last_op_zl__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Last inst_a -> Last inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<_).
+
+#[local] Definition Ord__Last_op_zlze__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Last inst_a -> Last inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<=_).
+
+#[local] Definition Ord__Last_op_zg__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Last inst_a -> Last inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>_).
+
+#[local] Definition Ord__Last_op_zgze__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Last inst_a -> Last inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>=_).
+
+#[local] Definition Ord__Last_compare {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Last inst_a -> Last inst_a -> comparison :=
+  GHC.Prim.coerce (GHC.Base.compare).
+
+#[local] Definition Ord__Last_max {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Last inst_a -> Last inst_a -> Last inst_a :=
+  GHC.Prim.coerce (GHC.Base.max).
+
+#[local] Definition Ord__Last_min {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Last inst_a -> Last inst_a -> Last inst_a :=
+  GHC.Prim.coerce (GHC.Base.min).
+
+#[global]
+Program Instance Ord__Last {a : Type} `{GHC.Base.Ord a}
+   : GHC.Base.Ord (Last a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zl____ := Ord__Last_op_zl__ ;
+           GHC.Base.op_zlze____ := Ord__Last_op_zlze__ ;
+           GHC.Base.op_zg____ := Ord__Last_op_zg__ ;
+           GHC.Base.op_zgze____ := Ord__Last_op_zgze__ ;
+           GHC.Base.compare__ := Ord__Last_compare ;
+           GHC.Base.max__ := Ord__Last_max ;
+           GHC.Base.min__ := Ord__Last_min |}.
+
+(* Skipping all instances of class `GHC.Show.Show', including
+   `Data.Semigroup.Show__Last' *)
+
+(* Skipping all instances of class `GHC.Read.Read', including
+   `Data.Semigroup.Read__Last' *)
+
+(* Skipping all instances of class `Data.Data.Data', including
+   `Data.Semigroup.Data__Last' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic', including
+   `Data.Semigroup.Generic__Last' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic1', including
+   `Data.Semigroup.Generic1__TYPE__Last__LiftedRep' *)
+
+(* Skipping all instances of class `GHC.Enum.Bounded', including
+   `Data.Semigroup.Bounded__First' *)
+
+Instance Unpeel_First a : HsToCoq.Unpeel.Unpeel (First a) a :=
+  HsToCoq.Unpeel.Build_Unpeel _ _ getFirst Mk_First.
+
+#[local] Definition Eq___First_op_zeze__ {inst_a : Type} `{GHC.Base.Eq_ inst_a}
+   : First inst_a -> First inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.==_).
+
+#[local] Definition Eq___First_op_zsze__ {inst_a : Type} `{GHC.Base.Eq_ inst_a}
+   : First inst_a -> First inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base./=_).
+
+#[global]
+Program Instance Eq___First {a : Type} `{GHC.Base.Eq_ a}
+   : GHC.Base.Eq_ (First a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zeze____ := Eq___First_op_zeze__ ;
+           GHC.Base.op_zsze____ := Eq___First_op_zsze__ |}.
+
+#[local] Definition Ord__First_op_zl__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : First inst_a -> First inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<_).
+
+#[local] Definition Ord__First_op_zlze__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : First inst_a -> First inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<=_).
+
+#[local] Definition Ord__First_op_zg__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : First inst_a -> First inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>_).
+
+#[local] Definition Ord__First_op_zgze__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : First inst_a -> First inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>=_).
+
+#[local] Definition Ord__First_compare {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : First inst_a -> First inst_a -> comparison :=
+  GHC.Prim.coerce (GHC.Base.compare).
+
+#[local] Definition Ord__First_max {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : First inst_a -> First inst_a -> First inst_a :=
+  GHC.Prim.coerce (GHC.Base.max).
+
+#[local] Definition Ord__First_min {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : First inst_a -> First inst_a -> First inst_a :=
+  GHC.Prim.coerce (GHC.Base.min).
+
+#[global]
+Program Instance Ord__First {a : Type} `{GHC.Base.Ord a}
+   : GHC.Base.Ord (First a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zl____ := Ord__First_op_zl__ ;
+           GHC.Base.op_zlze____ := Ord__First_op_zlze__ ;
+           GHC.Base.op_zg____ := Ord__First_op_zg__ ;
+           GHC.Base.op_zgze____ := Ord__First_op_zgze__ ;
+           GHC.Base.compare__ := Ord__First_compare ;
+           GHC.Base.max__ := Ord__First_max ;
+           GHC.Base.min__ := Ord__First_min |}.
+
+(* Skipping all instances of class `GHC.Show.Show', including
+   `Data.Semigroup.Show__First' *)
+
+(* Skipping all instances of class `GHC.Read.Read', including
+   `Data.Semigroup.Read__First' *)
+
+(* Skipping all instances of class `Data.Data.Data', including
+   `Data.Semigroup.Data__First' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic', including
+   `Data.Semigroup.Generic__First' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic1', including
+   `Data.Semigroup.Generic1__TYPE__First__LiftedRep' *)
+
+(* Skipping all instances of class `GHC.Show.Show', including
+   `Data.Semigroup.Show__Arg' *)
+
+(* Skipping all instances of class `GHC.Read.Read', including
+   `Data.Semigroup.Read__Arg' *)
+
+(* Skipping all instances of class `Data.Data.Data', including
+   `Data.Semigroup.Data__Arg' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic', including
+   `Data.Semigroup.Generic__Arg' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic1', including
+   `Data.Semigroup.Generic1__TYPE__Arg__LiftedRep' *)
+
+(* Skipping all instances of class `GHC.Enum.Bounded', including
+   `Data.Semigroup.Bounded__Max' *)
+
+Instance Unpeel_Max a : HsToCoq.Unpeel.Unpeel (Max a) a :=
+  HsToCoq.Unpeel.Build_Unpeel _ _ getMax Mk_Max.
+
+#[local] Definition Eq___Max_op_zeze__ {inst_a : Type} `{GHC.Base.Eq_ inst_a}
+   : Max inst_a -> Max inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.==_).
+
+#[local] Definition Eq___Max_op_zsze__ {inst_a : Type} `{GHC.Base.Eq_ inst_a}
+   : Max inst_a -> Max inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base./=_).
+
+#[global]
+Program Instance Eq___Max {a : Type} `{GHC.Base.Eq_ a} : GHC.Base.Eq_ (Max a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zeze____ := Eq___Max_op_zeze__ ;
+           GHC.Base.op_zsze____ := Eq___Max_op_zsze__ |}.
+
+#[local] Definition Ord__Max_op_zl__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Max inst_a -> Max inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<_).
+
+#[local] Definition Ord__Max_op_zlze__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Max inst_a -> Max inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<=_).
+
+#[local] Definition Ord__Max_op_zg__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Max inst_a -> Max inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>_).
+
+#[local] Definition Ord__Max_op_zgze__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Max inst_a -> Max inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>=_).
+
+#[local] Definition Ord__Max_compare {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Max inst_a -> Max inst_a -> comparison :=
+  GHC.Prim.coerce (GHC.Base.compare).
+
+#[local] Definition Ord__Max_max {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Max inst_a -> Max inst_a -> Max inst_a :=
+  GHC.Prim.coerce (GHC.Base.max).
+
+#[local] Definition Ord__Max_min {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Max inst_a -> Max inst_a -> Max inst_a :=
+  GHC.Prim.coerce (GHC.Base.min).
+
+#[global]
+Program Instance Ord__Max {a : Type} `{GHC.Base.Ord a} : GHC.Base.Ord (Max a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zl____ := Ord__Max_op_zl__ ;
+           GHC.Base.op_zlze____ := Ord__Max_op_zlze__ ;
+           GHC.Base.op_zg____ := Ord__Max_op_zg__ ;
+           GHC.Base.op_zgze____ := Ord__Max_op_zgze__ ;
+           GHC.Base.compare__ := Ord__Max_compare ;
+           GHC.Base.max__ := Ord__Max_max ;
+           GHC.Base.min__ := Ord__Max_min |}.
+
+(* Skipping all instances of class `GHC.Show.Show', including
+   `Data.Semigroup.Show__Max' *)
+
+(* Skipping all instances of class `GHC.Read.Read', including
+   `Data.Semigroup.Read__Max' *)
+
+(* Skipping all instances of class `Data.Data.Data', including
+   `Data.Semigroup.Data__Max' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic', including
+   `Data.Semigroup.Generic__Max' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic1', including
+   `Data.Semigroup.Generic1__TYPE__Max__LiftedRep' *)
+
+(* Skipping all instances of class `GHC.Enum.Bounded', including
+   `Data.Semigroup.Bounded__Min' *)
+
+Instance Unpeel_Min a : HsToCoq.Unpeel.Unpeel (Min a) a :=
+  HsToCoq.Unpeel.Build_Unpeel _ _ getMin Mk_Min.
+
+#[local] Definition Eq___Min_op_zeze__ {inst_a : Type} `{GHC.Base.Eq_ inst_a}
+   : Min inst_a -> Min inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.==_).
+
+#[local] Definition Eq___Min_op_zsze__ {inst_a : Type} `{GHC.Base.Eq_ inst_a}
+   : Min inst_a -> Min inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base./=_).
+
+#[global]
+Program Instance Eq___Min {a : Type} `{GHC.Base.Eq_ a} : GHC.Base.Eq_ (Min a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zeze____ := Eq___Min_op_zeze__ ;
+           GHC.Base.op_zsze____ := Eq___Min_op_zsze__ |}.
+
+#[local] Definition Ord__Min_op_zl__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Min inst_a -> Min inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<_).
+
+#[local] Definition Ord__Min_op_zlze__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Min inst_a -> Min inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<=_).
+
+#[local] Definition Ord__Min_op_zg__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Min inst_a -> Min inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>_).
+
+#[local] Definition Ord__Min_op_zgze__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Min inst_a -> Min inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>=_).
+
+#[local] Definition Ord__Min_compare {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Min inst_a -> Min inst_a -> comparison :=
+  GHC.Prim.coerce (GHC.Base.compare).
+
+#[local] Definition Ord__Min_max {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Min inst_a -> Min inst_a -> Min inst_a :=
+  GHC.Prim.coerce (GHC.Base.max).
+
+#[local] Definition Ord__Min_min {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Min inst_a -> Min inst_a -> Min inst_a :=
+  GHC.Prim.coerce (GHC.Base.min).
+
+#[global]
+Program Instance Ord__Min {a : Type} `{GHC.Base.Ord a} : GHC.Base.Ord (Min a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zl____ := Ord__Min_op_zl__ ;
+           GHC.Base.op_zlze____ := Ord__Min_op_zlze__ ;
+           GHC.Base.op_zg____ := Ord__Min_op_zg__ ;
+           GHC.Base.op_zgze____ := Ord__Min_op_zgze__ ;
+           GHC.Base.compare__ := Ord__Min_compare ;
+           GHC.Base.max__ := Ord__Min_max ;
+           GHC.Base.min__ := Ord__Min_min |}.
+
+(* Skipping all instances of class `GHC.Show.Show', including
+   `Data.Semigroup.Show__Min' *)
+
+(* Skipping all instances of class `GHC.Read.Read', including
+   `Data.Semigroup.Read__Min' *)
+
+(* Skipping all instances of class `Data.Data.Data', including
+   `Data.Semigroup.Data__Min' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic', including
+   `Data.Semigroup.Generic__Min' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic1', including
+   `Data.Semigroup.Generic1__TYPE__Min__LiftedRep' *)
+
 (* Skipping all instances of class `GHC.Enum.Enum', including
    `Data.Semigroup.Enum__Min' *)
 
@@ -1729,36 +2202,18 @@ Program Instance Monoid__Option {a : Type} `{GHC.Base.Semigroup a}
     | n, j, Mk_Option m => Data.Maybe.maybe n j m
     end.
 
-Instance Unpeel_Min a : HsToCoq.Unpeel.Unpeel (Min a) a :=
-  HsToCoq.Unpeel.Build_Unpeel _ _ getMin Mk_Min.
-
-Instance Unpeel_Max a : HsToCoq.Unpeel.Unpeel (Max a) a :=
-  HsToCoq.Unpeel.Build_Unpeel _ _ getMax Mk_Max.
-
-Instance Unpeel_First a : HsToCoq.Unpeel.Unpeel (First a) a :=
-  HsToCoq.Unpeel.Build_Unpeel _ _ getFirst Mk_First.
-
-Instance Unpeel_Last a : HsToCoq.Unpeel.Unpeel (Last a) a :=
-  HsToCoq.Unpeel.Build_Unpeel _ _ getLast Mk_Last.
-
-Instance Unpeel_WrappedMonoid a : HsToCoq.Unpeel.Unpeel (WrappedMonoid a) a :=
-  HsToCoq.Unpeel.Build_Unpeel _ _ unwrapMonoid WrapMonoid.
-
-Instance Unpeel_Option a : HsToCoq.Unpeel.Unpeel (Option a) (option a) :=
-  HsToCoq.Unpeel.Build_Unpeel _ _ getOption Mk_Option.
-
 (* External variables:
-     None Some Type bool false list negb option true Coq.Program.Basics.compose
-     Data.Bifoldable.Bifoldable Data.Bifoldable.bifoldMap__ Data.Bifoldable.bifold__
-     Data.Bifoldable.bifoldl__ Data.Bifoldable.bifoldr__ Data.Bifunctor.Bifunctor
-     Data.Bifunctor.bimap__ Data.Bifunctor.first__ Data.Bifunctor.second__
-     Data.Bitraversable.Bitraversable Data.Bitraversable.bitraverse__
-     Data.Foldable.Foldable Data.Foldable.foldMap'__ Data.Foldable.foldMap__
-     Data.Foldable.fold__ Data.Foldable.foldl'__ Data.Foldable.foldl__
-     Data.Foldable.foldr'__ Data.Foldable.foldr__ Data.Foldable.length__
-     Data.Foldable.null__ Data.Foldable.product__ Data.Foldable.sum__
-     Data.Foldable.toList__ Data.Functor.op_zlzdzg__ Data.Maybe.maybe
-     Data.SemigroupInternal.Endo Data.SemigroupInternal.Mk_Dual
+     None Some Type bool comparison false list negb option true
+     Coq.Program.Basics.compose Data.Bifoldable.Bifoldable
+     Data.Bifoldable.bifoldMap__ Data.Bifoldable.bifold__ Data.Bifoldable.bifoldl__
+     Data.Bifoldable.bifoldr__ Data.Bifunctor.Bifunctor Data.Bifunctor.bimap__
+     Data.Bifunctor.first__ Data.Bifunctor.second__ Data.Bitraversable.Bitraversable
+     Data.Bitraversable.bitraverse__ Data.Foldable.Foldable Data.Foldable.foldMap'__
+     Data.Foldable.foldMap__ Data.Foldable.fold__ Data.Foldable.foldl'__
+     Data.Foldable.foldl__ Data.Foldable.foldr'__ Data.Foldable.foldr__
+     Data.Foldable.length__ Data.Foldable.null__ Data.Foldable.product__
+     Data.Foldable.sum__ Data.Foldable.toList__ Data.Functor.op_zlzdzg__
+     Data.Maybe.maybe Data.SemigroupInternal.Endo Data.SemigroupInternal.Mk_Dual
      Data.SemigroupInternal.Mk_Endo Data.SemigroupInternal.Mk_Product
      Data.SemigroupInternal.Mk_Sum Data.SemigroupInternal.appEndo
      Data.SemigroupInternal.getDual Data.SemigroupInternal.getProduct
@@ -1766,14 +2221,17 @@ Instance Unpeel_Option a : HsToCoq.Unpeel.Unpeel (Option a) (option a) :=
      Data.Traversable.mapM__ Data.Traversable.sequenceA__ Data.Traversable.sequence__
      Data.Traversable.traverse__ GHC.Base.Applicative GHC.Base.Eq_ GHC.Base.Functor
      GHC.Base.Monad GHC.Base.Monoid GHC.Base.Ord GHC.Base.Semigroup GHC.Base.build'
-     GHC.Base.const GHC.Base.flip GHC.Base.fmap GHC.Base.fmap__ GHC.Base.foldr
-     GHC.Base.id GHC.Base.liftA2 GHC.Base.liftA2__ GHC.Base.mappend
-     GHC.Base.mappend__ GHC.Base.max GHC.Base.mconcat__ GHC.Base.mempty
-     GHC.Base.mempty__ GHC.Base.min GHC.Base.op_z2218U__ GHC.Base.op_zeze__
-     GHC.Base.op_zeze____ GHC.Base.op_zgzg____ GHC.Base.op_zgzgze____
-     GHC.Base.op_zlzd____ GHC.Base.op_zlzlzgzg__ GHC.Base.op_zlzlzgzg____
-     GHC.Base.op_zlztzg__ GHC.Base.op_zlztzg____ GHC.Base.op_zsze____
-     GHC.Base.op_ztzg__ GHC.Base.op_ztzg____ GHC.Base.pure GHC.Base.pure__
-     GHC.Base.return___ GHC.Num.Int GHC.Num.Num GHC.Num.fromInteger GHC.Num.op_zp__
-     GHC.Prim.coerce HsToCoq.Unpeel.Build_Unpeel HsToCoq.Unpeel.Unpeel
+     GHC.Base.compare GHC.Base.compare__ GHC.Base.const GHC.Base.flip GHC.Base.fmap
+     GHC.Base.fmap__ GHC.Base.foldr GHC.Base.id GHC.Base.liftA2 GHC.Base.liftA2__
+     GHC.Base.mappend GHC.Base.mappend__ GHC.Base.max GHC.Base.max__
+     GHC.Base.mconcat__ GHC.Base.mempty GHC.Base.mempty__ GHC.Base.min GHC.Base.min__
+     GHC.Base.op_z2218U__ GHC.Base.op_zeze__ GHC.Base.op_zeze____ GHC.Base.op_zg__
+     GHC.Base.op_zg____ GHC.Base.op_zgze__ GHC.Base.op_zgze____ GHC.Base.op_zgzg____
+     GHC.Base.op_zgzgze____ GHC.Base.op_zl__ GHC.Base.op_zl____ GHC.Base.op_zlzd____
+     GHC.Base.op_zlze__ GHC.Base.op_zlze____ GHC.Base.op_zlzlzgzg__
+     GHC.Base.op_zlzlzgzg____ GHC.Base.op_zlztzg__ GHC.Base.op_zlztzg____
+     GHC.Base.op_zsze__ GHC.Base.op_zsze____ GHC.Base.op_ztzg__ GHC.Base.op_ztzg____
+     GHC.Base.pure GHC.Base.pure__ GHC.Base.return___ GHC.Num.Int GHC.Num.Num
+     GHC.Num.fromInteger GHC.Num.op_zp__ GHC.Prim.coerce HsToCoq.Unpeel.Build_Unpeel
+     HsToCoq.Unpeel.Unpeel
 *)
diff --git a/base/Data/SemigroupInternal.v b/base/Data/SemigroupInternal.v
index 1cde8c30..0f226ace 100644
--- a/base/Data/SemigroupInternal.v
+++ b/base/Data/SemigroupInternal.v
@@ -98,6 +98,525 @@ Instance Unpeel_Alt (k : Type) (f : k -> Type) (a : k) : HsToCoq.Unpeel.Unpeel (
 
 (* Converted value declarations: *)
 
+(* Skipping all instances of class `GHC.Generics.Generic', including
+   `Data.SemigroupInternal.Generic__Alt' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic1', including
+   `Data.SemigroupInternal.Generic1__Alt__5' *)
+
+(* Skipping all instances of class `GHC.Read.Read', including
+   `Data.SemigroupInternal.Read__Alt' *)
+
+(* Skipping all instances of class `GHC.Show.Show', including
+   `Data.SemigroupInternal.Show__Alt' *)
+
+#[local] Definition Eq___Alt_op_zeze__ {inst_k : Type} {inst_f : inst_k -> Type}
+  {inst_a : inst_k} `{GHC.Base.Eq_ (inst_f inst_a)}
+   : Alt inst_f inst_a -> Alt inst_f inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.==_).
+
+#[local] Definition Eq___Alt_op_zsze__ {inst_k : Type} {inst_f : inst_k -> Type}
+  {inst_a : inst_k} `{GHC.Base.Eq_ (inst_f inst_a)}
+   : Alt inst_f inst_a -> Alt inst_f inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base./=_).
+
+#[global]
+Program Instance Eq___Alt {k : Type} {f : k -> Type} {a : k} `{GHC.Base.Eq_ (f
+                                                                             a)}
+   : GHC.Base.Eq_ (Alt f a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zeze____ := Eq___Alt_op_zeze__ ;
+           GHC.Base.op_zsze____ := Eq___Alt_op_zsze__ |}.
+
+#[local] Definition Ord__Alt_op_zl__ {inst_k : Type} {inst_f : inst_k -> Type}
+  {inst_a : inst_k} `{GHC.Base.Ord (inst_f inst_a)}
+   : Alt inst_f inst_a -> Alt inst_f inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<_).
+
+#[local] Definition Ord__Alt_op_zlze__ {inst_k : Type} {inst_f : inst_k -> Type}
+  {inst_a : inst_k} `{GHC.Base.Ord (inst_f inst_a)}
+   : Alt inst_f inst_a -> Alt inst_f inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<=_).
+
+#[local] Definition Ord__Alt_op_zg__ {inst_k : Type} {inst_f : inst_k -> Type}
+  {inst_a : inst_k} `{GHC.Base.Ord (inst_f inst_a)}
+   : Alt inst_f inst_a -> Alt inst_f inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>_).
+
+#[local] Definition Ord__Alt_op_zgze__ {inst_k : Type} {inst_f : inst_k -> Type}
+  {inst_a : inst_k} `{GHC.Base.Ord (inst_f inst_a)}
+   : Alt inst_f inst_a -> Alt inst_f inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>=_).
+
+#[local] Definition Ord__Alt_compare {inst_k : Type} {inst_f : inst_k -> Type}
+  {inst_a : inst_k} `{GHC.Base.Ord (inst_f inst_a)}
+   : Alt inst_f inst_a -> Alt inst_f inst_a -> comparison :=
+  GHC.Prim.coerce (GHC.Base.compare).
+
+#[local] Definition Ord__Alt_max {inst_k : Type} {inst_f : inst_k -> Type}
+  {inst_a : inst_k} `{GHC.Base.Ord (inst_f inst_a)}
+   : Alt inst_f inst_a -> Alt inst_f inst_a -> Alt inst_f inst_a :=
+  GHC.Prim.coerce (GHC.Base.max).
+
+#[local] Definition Ord__Alt_min {inst_k : Type} {inst_f : inst_k -> Type}
+  {inst_a : inst_k} `{GHC.Base.Ord (inst_f inst_a)}
+   : Alt inst_f inst_a -> Alt inst_f inst_a -> Alt inst_f inst_a :=
+  GHC.Prim.coerce (GHC.Base.min).
+
+#[global]
+Program Instance Ord__Alt {k : Type} {f : k -> Type} {a : k} `{GHC.Base.Ord (f
+                                                                             a)}
+   : GHC.Base.Ord (Alt f a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zl____ := Ord__Alt_op_zl__ ;
+           GHC.Base.op_zlze____ := Ord__Alt_op_zlze__ ;
+           GHC.Base.op_zg____ := Ord__Alt_op_zg__ ;
+           GHC.Base.op_zgze____ := Ord__Alt_op_zgze__ ;
+           GHC.Base.compare__ := Ord__Alt_compare ;
+           GHC.Base.max__ := Ord__Alt_max ;
+           GHC.Base.min__ := Ord__Alt_min |}.
+
+(* Skipping all instances of class `GHC.Num.Num', including
+   `Data.SemigroupInternal.Num__Alt' *)
+
+(* Skipping all instances of class `GHC.Enum.Enum', including
+   `Data.SemigroupInternal.Enum__Alt' *)
+
+#[local] Definition Monad__Alt_op_zgzg__ {inst_f : Type -> Type}
+  `{GHC.Base.Monad inst_f}
+   : forall {a : Type},
+     forall {b : Type}, Alt inst_f a -> Alt inst_f b -> Alt inst_f b :=
+  fun {a : Type} {b : Type} => GHC.Prim.coerce (_GHC.Base.>>_).
+
+#[local] Definition Monad__Alt_op_zgzgze__ {inst_f : Type -> Type}
+  `{GHC.Base.Monad inst_f}
+   : forall {a : Type},
+     forall {b : Type}, Alt inst_f a -> (a -> Alt inst_f b) -> Alt inst_f b :=
+  fun {a : Type} {b : Type} => GHC.Prim.coerce (_GHC.Base.>>=_).
+
+#[local] Definition Monad__Alt_return_ {inst_f : Type -> Type} `{GHC.Base.Monad
+  inst_f}
+   : forall {a : Type}, a -> Alt inst_f a :=
+  fun {a : Type} => GHC.Prim.coerce (GHC.Base.return_).
+
+#[local] Definition Applicative__Alt_liftA2 {inst_f : Type -> Type}
+  `{GHC.Base.Applicative inst_f}
+   : forall {a : Type},
+     forall {b : Type},
+     forall {c : Type},
+     (a -> b -> c) -> Alt inst_f a -> Alt inst_f b -> Alt inst_f c :=
+  fun {a : Type} {b : Type} {c : Type} => GHC.Prim.coerce (GHC.Base.liftA2).
+
+#[local] Definition Applicative__Alt_op_zlztzg__ {inst_f : Type -> Type}
+  `{GHC.Base.Applicative inst_f}
+   : forall {a : Type},
+     forall {b : Type}, Alt inst_f (a -> b) -> Alt inst_f a -> Alt inst_f b :=
+  fun {a : Type} {b : Type} => GHC.Prim.coerce (_GHC.Base.<*>_).
+
+#[local] Definition Applicative__Alt_op_ztzg__ {inst_f : Type -> Type}
+  `{GHC.Base.Applicative inst_f}
+   : forall {a : Type},
+     forall {b : Type}, Alt inst_f a -> Alt inst_f b -> Alt inst_f b :=
+  fun {a : Type} {b : Type} => GHC.Prim.coerce (_GHC.Base.*>_).
+
+#[local] Definition Applicative__Alt_pure {inst_f : Type -> Type}
+  `{GHC.Base.Applicative inst_f}
+   : forall {a : Type}, a -> Alt inst_f a :=
+  fun {a : Type} => GHC.Prim.coerce (GHC.Base.pure).
+
+#[local] Definition Functor__Alt_fmap {inst_f : Type -> Type} `{GHC.Base.Functor
+  inst_f}
+   : forall {a : Type},
+     forall {b : Type}, (a -> b) -> Alt inst_f a -> Alt inst_f b :=
+  fun {a : Type} {b : Type} => GHC.Prim.coerce (GHC.Base.fmap).
+
+#[local] Definition Functor__Alt_op_zlzd__ {inst_f : Type -> Type}
+  `{GHC.Base.Functor inst_f}
+   : forall {a : Type}, forall {b : Type}, a -> Alt inst_f b -> Alt inst_f a :=
+  fun {a : Type} {b : Type} => GHC.Prim.coerce (_GHC.Base.<$_).
+
+#[global]
+Program Instance Functor__Alt {f : Type -> Type} `{GHC.Base.Functor f}
+   : GHC.Base.Functor (Alt f) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.fmap__ := fun {a : Type} {b : Type} => Functor__Alt_fmap ;
+           GHC.Base.op_zlzd____ := fun {a : Type} {b : Type} => Functor__Alt_op_zlzd__ |}.
+
+#[global]
+Program Instance Applicative__Alt {f : Type -> Type} `{GHC.Base.Applicative f}
+   : GHC.Base.Applicative (Alt f) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.liftA2__ := fun {a : Type} {b : Type} {c : Type} =>
+             Applicative__Alt_liftA2 ;
+           GHC.Base.op_zlztzg____ := fun {a : Type} {b : Type} =>
+             Applicative__Alt_op_zlztzg__ ;
+           GHC.Base.op_ztzg____ := fun {a : Type} {b : Type} =>
+             Applicative__Alt_op_ztzg__ ;
+           GHC.Base.pure__ := fun {a : Type} => Applicative__Alt_pure |}.
+
+#[global]
+Program Instance Monad__Alt {f : Type -> Type} `{GHC.Base.Monad f}
+   : GHC.Base.Monad (Alt f) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zgzg____ := fun {a : Type} {b : Type} =>
+             Monad__Alt_op_zgzg__ ;
+           GHC.Base.op_zgzgze____ := fun {a : Type} {b : Type} => Monad__Alt_op_zgzgze__ ;
+           GHC.Base.return___ := fun {a : Type} => Monad__Alt_return_ |}.
+
+(* Skipping all instances of class `GHC.Base.MonadPlus', including
+   `Data.SemigroupInternal.MonadPlus__Alt' *)
+
+(* Skipping all instances of class `GHC.Base.Alternative', including
+   `Data.SemigroupInternal.Alternative__Alt' *)
+
+Instance Unpeel_Product a : HsToCoq.Unpeel.Unpeel (Product a) a :=
+  HsToCoq.Unpeel.Build_Unpeel _ _ getProduct Mk_Product.
+
+#[local] Definition Eq___Product_op_zeze__ {inst_a : Type} `{GHC.Base.Eq_
+  inst_a}
+   : Product inst_a -> Product inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.==_).
+
+#[local] Definition Eq___Product_op_zsze__ {inst_a : Type} `{GHC.Base.Eq_
+  inst_a}
+   : Product inst_a -> Product inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base./=_).
+
+#[global]
+Program Instance Eq___Product {a : Type} `{GHC.Base.Eq_ a}
+   : GHC.Base.Eq_ (Product a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zeze____ := Eq___Product_op_zeze__ ;
+           GHC.Base.op_zsze____ := Eq___Product_op_zsze__ |}.
+
+#[local] Definition Ord__Product_op_zl__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Product inst_a -> Product inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<_).
+
+#[local] Definition Ord__Product_op_zlze__ {inst_a : Type} `{GHC.Base.Ord
+  inst_a}
+   : Product inst_a -> Product inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<=_).
+
+#[local] Definition Ord__Product_op_zg__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Product inst_a -> Product inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>_).
+
+#[local] Definition Ord__Product_op_zgze__ {inst_a : Type} `{GHC.Base.Ord
+  inst_a}
+   : Product inst_a -> Product inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>=_).
+
+#[local] Definition Ord__Product_compare {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Product inst_a -> Product inst_a -> comparison :=
+  GHC.Prim.coerce (GHC.Base.compare).
+
+#[local] Definition Ord__Product_max {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Product inst_a -> Product inst_a -> Product inst_a :=
+  GHC.Prim.coerce (GHC.Base.max).
+
+#[local] Definition Ord__Product_min {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Product inst_a -> Product inst_a -> Product inst_a :=
+  GHC.Prim.coerce (GHC.Base.min).
+
+#[global]
+Program Instance Ord__Product {a : Type} `{GHC.Base.Ord a}
+   : GHC.Base.Ord (Product a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zl____ := Ord__Product_op_zl__ ;
+           GHC.Base.op_zlze____ := Ord__Product_op_zlze__ ;
+           GHC.Base.op_zg____ := Ord__Product_op_zg__ ;
+           GHC.Base.op_zgze____ := Ord__Product_op_zgze__ ;
+           GHC.Base.compare__ := Ord__Product_compare ;
+           GHC.Base.max__ := Ord__Product_max ;
+           GHC.Base.min__ := Ord__Product_min |}.
+
+(* Skipping all instances of class `GHC.Read.Read', including
+   `Data.SemigroupInternal.Read__Product' *)
+
+(* Skipping all instances of class `GHC.Show.Show', including
+   `Data.SemigroupInternal.Show__Product' *)
+
+(* Skipping all instances of class `GHC.Enum.Bounded', including
+   `Data.SemigroupInternal.Bounded__Product' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic', including
+   `Data.SemigroupInternal.Generic__Product' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic1', including
+   `Data.SemigroupInternal.Generic1__TYPE__Product__LiftedRep' *)
+
+(* Skipping all instances of class `GHC.Num.Num', including
+   `Data.SemigroupInternal.Num__Product' *)
+
+Instance Unpeel_Sum a : HsToCoq.Unpeel.Unpeel (Sum a) a :=
+  HsToCoq.Unpeel.Build_Unpeel _ _ getSum Mk_Sum.
+
+#[local] Definition Eq___Sum_op_zeze__ {inst_a : Type} `{GHC.Base.Eq_ inst_a}
+   : Sum inst_a -> Sum inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.==_).
+
+#[local] Definition Eq___Sum_op_zsze__ {inst_a : Type} `{GHC.Base.Eq_ inst_a}
+   : Sum inst_a -> Sum inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base./=_).
+
+#[global]
+Program Instance Eq___Sum {a : Type} `{GHC.Base.Eq_ a} : GHC.Base.Eq_ (Sum a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zeze____ := Eq___Sum_op_zeze__ ;
+           GHC.Base.op_zsze____ := Eq___Sum_op_zsze__ |}.
+
+#[local] Definition Ord__Sum_op_zl__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Sum inst_a -> Sum inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<_).
+
+#[local] Definition Ord__Sum_op_zlze__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Sum inst_a -> Sum inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<=_).
+
+#[local] Definition Ord__Sum_op_zg__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Sum inst_a -> Sum inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>_).
+
+#[local] Definition Ord__Sum_op_zgze__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Sum inst_a -> Sum inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>=_).
+
+#[local] Definition Ord__Sum_compare {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Sum inst_a -> Sum inst_a -> comparison :=
+  GHC.Prim.coerce (GHC.Base.compare).
+
+#[local] Definition Ord__Sum_max {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Sum inst_a -> Sum inst_a -> Sum inst_a :=
+  GHC.Prim.coerce (GHC.Base.max).
+
+#[local] Definition Ord__Sum_min {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Sum inst_a -> Sum inst_a -> Sum inst_a :=
+  GHC.Prim.coerce (GHC.Base.min).
+
+#[global]
+Program Instance Ord__Sum {a : Type} `{GHC.Base.Ord a} : GHC.Base.Ord (Sum a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zl____ := Ord__Sum_op_zl__ ;
+           GHC.Base.op_zlze____ := Ord__Sum_op_zlze__ ;
+           GHC.Base.op_zg____ := Ord__Sum_op_zg__ ;
+           GHC.Base.op_zgze____ := Ord__Sum_op_zgze__ ;
+           GHC.Base.compare__ := Ord__Sum_compare ;
+           GHC.Base.max__ := Ord__Sum_max ;
+           GHC.Base.min__ := Ord__Sum_min |}.
+
+(* Skipping all instances of class `GHC.Read.Read', including
+   `Data.SemigroupInternal.Read__Sum' *)
+
+(* Skipping all instances of class `GHC.Show.Show', including
+   `Data.SemigroupInternal.Show__Sum' *)
+
+(* Skipping all instances of class `GHC.Enum.Bounded', including
+   `Data.SemigroupInternal.Bounded__Sum' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic', including
+   `Data.SemigroupInternal.Generic__Sum' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic1', including
+   `Data.SemigroupInternal.Generic1__TYPE__Sum__LiftedRep' *)
+
+(* Skipping all instances of class `GHC.Num.Num', including
+   `Data.SemigroupInternal.Num__Sum' *)
+
+Instance Unpeel_Any : HsToCoq.Unpeel.Unpeel Any bool :=
+  HsToCoq.Unpeel.Build_Unpeel _ _ getAny Mk_Any.
+
+#[local] Definition Eq___Any_op_zeze__ : Any -> Any -> bool :=
+  GHC.Prim.coerce (_GHC.Base.==_).
+
+#[local] Definition Eq___Any_op_zsze__ : Any -> Any -> bool :=
+  GHC.Prim.coerce (_GHC.Base./=_).
+
+#[global]
+Program Instance Eq___Any : GHC.Base.Eq_ Any :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zeze____ := Eq___Any_op_zeze__ ;
+           GHC.Base.op_zsze____ := Eq___Any_op_zsze__ |}.
+
+#[local] Definition Ord__Any_op_zl__ : Any -> Any -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<_).
+
+#[local] Definition Ord__Any_op_zlze__ : Any -> Any -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<=_).
+
+#[local] Definition Ord__Any_op_zg__ : Any -> Any -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>_).
+
+#[local] Definition Ord__Any_op_zgze__ : Any -> Any -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>=_).
+
+#[local] Definition Ord__Any_compare : Any -> Any -> comparison :=
+  GHC.Prim.coerce (GHC.Base.compare).
+
+#[local] Definition Ord__Any_max : Any -> Any -> Any :=
+  GHC.Prim.coerce (GHC.Base.max).
+
+#[local] Definition Ord__Any_min : Any -> Any -> Any :=
+  GHC.Prim.coerce (GHC.Base.min).
+
+#[global]
+Program Instance Ord__Any : GHC.Base.Ord Any :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zl____ := Ord__Any_op_zl__ ;
+           GHC.Base.op_zlze____ := Ord__Any_op_zlze__ ;
+           GHC.Base.op_zg____ := Ord__Any_op_zg__ ;
+           GHC.Base.op_zgze____ := Ord__Any_op_zgze__ ;
+           GHC.Base.compare__ := Ord__Any_compare ;
+           GHC.Base.max__ := Ord__Any_max ;
+           GHC.Base.min__ := Ord__Any_min |}.
+
+(* Skipping all instances of class `GHC.Read.Read', including
+   `Data.SemigroupInternal.Read__Any' *)
+
+(* Skipping all instances of class `GHC.Show.Show', including
+   `Data.SemigroupInternal.Show__Any' *)
+
+(* Skipping all instances of class `GHC.Enum.Bounded', including
+   `Data.SemigroupInternal.Bounded__Any' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic', including
+   `Data.SemigroupInternal.Generic__Any' *)
+
+Instance Unpeel_All : HsToCoq.Unpeel.Unpeel All bool :=
+  HsToCoq.Unpeel.Build_Unpeel _ _ getAll Mk_All.
+
+#[local] Definition Eq___All_op_zeze__ : All -> All -> bool :=
+  GHC.Prim.coerce (_GHC.Base.==_).
+
+#[local] Definition Eq___All_op_zsze__ : All -> All -> bool :=
+  GHC.Prim.coerce (_GHC.Base./=_).
+
+#[global]
+Program Instance Eq___All : GHC.Base.Eq_ All :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zeze____ := Eq___All_op_zeze__ ;
+           GHC.Base.op_zsze____ := Eq___All_op_zsze__ |}.
+
+#[local] Definition Ord__All_op_zl__ : All -> All -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<_).
+
+#[local] Definition Ord__All_op_zlze__ : All -> All -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<=_).
+
+#[local] Definition Ord__All_op_zg__ : All -> All -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>_).
+
+#[local] Definition Ord__All_op_zgze__ : All -> All -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>=_).
+
+#[local] Definition Ord__All_compare : All -> All -> comparison :=
+  GHC.Prim.coerce (GHC.Base.compare).
+
+#[local] Definition Ord__All_max : All -> All -> All :=
+  GHC.Prim.coerce (GHC.Base.max).
+
+#[local] Definition Ord__All_min : All -> All -> All :=
+  GHC.Prim.coerce (GHC.Base.min).
+
+#[global]
+Program Instance Ord__All : GHC.Base.Ord All :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zl____ := Ord__All_op_zl__ ;
+           GHC.Base.op_zlze____ := Ord__All_op_zlze__ ;
+           GHC.Base.op_zg____ := Ord__All_op_zg__ ;
+           GHC.Base.op_zgze____ := Ord__All_op_zgze__ ;
+           GHC.Base.compare__ := Ord__All_compare ;
+           GHC.Base.max__ := Ord__All_max ;
+           GHC.Base.min__ := Ord__All_min |}.
+
+(* Skipping all instances of class `GHC.Read.Read', including
+   `Data.SemigroupInternal.Read__All' *)
+
+(* Skipping all instances of class `GHC.Show.Show', including
+   `Data.SemigroupInternal.Show__All' *)
+
+(* Skipping all instances of class `GHC.Enum.Bounded', including
+   `Data.SemigroupInternal.Bounded__All' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic', including
+   `Data.SemigroupInternal.Generic__All' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic', including
+   `Data.SemigroupInternal.Generic__Endo' *)
+
+Instance Unpeel_Dual a : HsToCoq.Unpeel.Unpeel (Dual a) a :=
+  HsToCoq.Unpeel.Build_Unpeel _ _ getDual Mk_Dual.
+
+#[local] Definition Eq___Dual_op_zeze__ {inst_a : Type} `{GHC.Base.Eq_ inst_a}
+   : Dual inst_a -> Dual inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.==_).
+
+#[local] Definition Eq___Dual_op_zsze__ {inst_a : Type} `{GHC.Base.Eq_ inst_a}
+   : Dual inst_a -> Dual inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base./=_).
+
+#[global]
+Program Instance Eq___Dual {a : Type} `{GHC.Base.Eq_ a}
+   : GHC.Base.Eq_ (Dual a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zeze____ := Eq___Dual_op_zeze__ ;
+           GHC.Base.op_zsze____ := Eq___Dual_op_zsze__ |}.
+
+#[local] Definition Ord__Dual_op_zl__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Dual inst_a -> Dual inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<_).
+
+#[local] Definition Ord__Dual_op_zlze__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Dual inst_a -> Dual inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.<=_).
+
+#[local] Definition Ord__Dual_op_zg__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Dual inst_a -> Dual inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>_).
+
+#[local] Definition Ord__Dual_op_zgze__ {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Dual inst_a -> Dual inst_a -> bool :=
+  GHC.Prim.coerce (_GHC.Base.>=_).
+
+#[local] Definition Ord__Dual_compare {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Dual inst_a -> Dual inst_a -> comparison :=
+  GHC.Prim.coerce (GHC.Base.compare).
+
+#[local] Definition Ord__Dual_max {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Dual inst_a -> Dual inst_a -> Dual inst_a :=
+  GHC.Prim.coerce (GHC.Base.max).
+
+#[local] Definition Ord__Dual_min {inst_a : Type} `{GHC.Base.Ord inst_a}
+   : Dual inst_a -> Dual inst_a -> Dual inst_a :=
+  GHC.Prim.coerce (GHC.Base.min).
+
+#[global]
+Program Instance Ord__Dual {a : Type} `{GHC.Base.Ord a}
+   : GHC.Base.Ord (Dual a) :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zl____ := Ord__Dual_op_zl__ ;
+           GHC.Base.op_zlze____ := Ord__Dual_op_zlze__ ;
+           GHC.Base.op_zg____ := Ord__Dual_op_zg__ ;
+           GHC.Base.op_zgze____ := Ord__Dual_op_zgze__ ;
+           GHC.Base.compare__ := Ord__Dual_compare ;
+           GHC.Base.max__ := Ord__Dual_max ;
+           GHC.Base.min__ := Ord__Dual_min |}.
+
+(* Skipping all instances of class `GHC.Read.Read', including
+   `Data.SemigroupInternal.Read__Dual' *)
+
+(* Skipping all instances of class `GHC.Show.Show', including
+   `Data.SemigroupInternal.Show__Dual' *)
+
+(* Skipping all instances of class `GHC.Enum.Bounded', including
+   `Data.SemigroupInternal.Bounded__Dual' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic', including
+   `Data.SemigroupInternal.Generic__Dual' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic1', including
+   `Data.SemigroupInternal.Generic1__TYPE__Dual__LiftedRep' *)
+
 #[local] Definition Semigroup__Dual_op_zlzlzgzg__ {inst_a : Type}
   `{GHC.Base.Semigroup inst_a}
    : Dual inst_a -> Dual inst_a -> Dual inst_a :=
@@ -501,30 +1020,21 @@ Program Instance Monad__Product : GHC.Base.Monad Product :=
 
 (* Skipping definition `Data.SemigroupInternal.stimesList' *)
 
-Instance Unpeel_Sum a : HsToCoq.Unpeel.Unpeel (Sum a) a :=
-  HsToCoq.Unpeel.Build_Unpeel _ _ getSum Mk_Sum.
-
-Instance Unpeel_Product a : HsToCoq.Unpeel.Unpeel (Product a) a :=
-  HsToCoq.Unpeel.Build_Unpeel _ _ getProduct Mk_Product.
-
-Instance Unpeel_All : HsToCoq.Unpeel.Unpeel All bool :=
-  HsToCoq.Unpeel.Build_Unpeel _ _ getAll Mk_All.
-
-Instance Unpeel_Any : HsToCoq.Unpeel.Unpeel Any bool :=
-  HsToCoq.Unpeel.Build_Unpeel _ _ getAny Mk_Any.
-
-Instance Unpeel_Dual a : HsToCoq.Unpeel.Unpeel (Dual a) a :=
-  HsToCoq.Unpeel.Build_Unpeel _ _ getDual Mk_Dual.
-
 (* External variables:
-     Eq Gt Lt Type andb bool false list orb true GHC.Base.Applicative
-     GHC.Base.Functor GHC.Base.Monad GHC.Base.Monoid GHC.Base.Semigroup
-     GHC.Base.compare GHC.Base.const GHC.Base.fmap GHC.Base.fmap__ GHC.Base.foldr
-     GHC.Base.id GHC.Base.liftA2__ GHC.Base.mappend__ GHC.Base.mconcat__
-     GHC.Base.mempty GHC.Base.mempty__ GHC.Base.op_z2218U__ GHC.Base.op_zgzg____
-     GHC.Base.op_zgzgze____ GHC.Base.op_zlzd__ GHC.Base.op_zlzd____
-     GHC.Base.op_zlzlzgzg__ GHC.Base.op_zlzlzgzg____ GHC.Base.op_zlztzg____
-     GHC.Base.op_ztzg____ GHC.Base.pure GHC.Base.pure__ GHC.Base.return___
+     Eq Gt Lt Type andb bool comparison false list orb true GHC.Base.Applicative
+     GHC.Base.Eq_ GHC.Base.Functor GHC.Base.Monad GHC.Base.Monoid GHC.Base.Ord
+     GHC.Base.Semigroup GHC.Base.compare GHC.Base.compare__ GHC.Base.const
+     GHC.Base.fmap GHC.Base.fmap__ GHC.Base.foldr GHC.Base.id GHC.Base.liftA2
+     GHC.Base.liftA2__ GHC.Base.mappend__ GHC.Base.max GHC.Base.max__
+     GHC.Base.mconcat__ GHC.Base.mempty GHC.Base.mempty__ GHC.Base.min GHC.Base.min__
+     GHC.Base.op_z2218U__ GHC.Base.op_zeze__ GHC.Base.op_zeze____ GHC.Base.op_zg__
+     GHC.Base.op_zg____ GHC.Base.op_zgze__ GHC.Base.op_zgze____ GHC.Base.op_zgzg__
+     GHC.Base.op_zgzg____ GHC.Base.op_zgzgze__ GHC.Base.op_zgzgze____
+     GHC.Base.op_zl__ GHC.Base.op_zl____ GHC.Base.op_zlzd__ GHC.Base.op_zlzd____
+     GHC.Base.op_zlze__ GHC.Base.op_zlze____ GHC.Base.op_zlzlzgzg__
+     GHC.Base.op_zlzlzgzg____ GHC.Base.op_zlztzg__ GHC.Base.op_zlztzg____
+     GHC.Base.op_zsze__ GHC.Base.op_zsze____ GHC.Base.op_ztzg__ GHC.Base.op_ztzg____
+     GHC.Base.pure GHC.Base.pure__ GHC.Base.return_ GHC.Base.return___
      GHC.Err.errorWithoutStackTrace GHC.Num.Num GHC.Num.fromInteger GHC.Num.op_zp__
      GHC.Num.op_zt__ GHC.Prim.coerce GHC.Real.Integral HsToCoq.Err.Build_Default
      HsToCoq.Err.Default HsToCoq.Err.default HsToCoq.Unpeel.Build_Unpeel
diff --git a/base/Data/Traversable.v b/base/Data/Traversable.v
index ed32dd32..d3891990 100644
--- a/base/Data/Traversable.v
+++ b/base/Data/Traversable.v
@@ -16,7 +16,7 @@ Require Data.Either.
 Require Data.Foldable.
 Require Data.Functor.
 Require Data.Functor.Const.
-Require Data.Functor.Identity.
+Require Import Data.Functor.Identity.
 Require Data.Functor.Utils.
 Require Data.Monoid.
 Require Data.Ord.
@@ -126,335 +126,23 @@ Program Instance Traversable__Down : Traversable Data.Ord.Down :=
            `{GHC.Base.Applicative f} =>
              Traversable__Down_traverse |}.
 
-#[local] Definition Traversable__UWord_traverse
-   : forall {f : Type -> Type},
-     forall {a : Type},
-     forall {b : Type},
-     forall `{GHC.Base.Applicative f},
-     (a -> f b) -> GHC.Generics.UWord a -> f (GHC.Generics.UWord b) :=
-  fun {f : Type -> Type} {a : Type} {b : Type} `{GHC.Base.Applicative f} =>
-    fun arg_0__ arg_1__ =>
-      match arg_0__, arg_1__ with
-      | f, GHC.Generics.UWord a1 => GHC.Base.pure (GHC.Generics.UWord a1)
-      end.
-
-#[local] Definition Traversable__UWord_mapM
-   : forall {m : Type -> Type},
-     forall {a : Type},
-     forall {b : Type},
-     forall `{GHC.Base.Monad m},
-     (a -> m b) -> GHC.Generics.UWord a -> m (GHC.Generics.UWord b) :=
-  fun {m : Type -> Type} {a : Type} {b : Type} `{GHC.Base.Monad m} =>
-    Traversable__UWord_traverse.
-
-#[local] Definition Traversable__UWord_sequenceA
-   : forall {f : Type -> Type},
-     forall {a : Type},
-     forall `{GHC.Base.Applicative f},
-     GHC.Generics.UWord (f a) -> f (GHC.Generics.UWord a) :=
-  fun {f : Type -> Type} {a : Type} `{GHC.Base.Applicative f} =>
-    Traversable__UWord_traverse GHC.Base.id.
-
-#[local] Definition Traversable__UWord_sequence
-   : forall {m : Type -> Type},
-     forall {a : Type},
-     forall `{GHC.Base.Monad m},
-     GHC.Generics.UWord (m a) -> m (GHC.Generics.UWord a) :=
-  fun {m : Type -> Type} {a : Type} `{GHC.Base.Monad m} =>
-    Traversable__UWord_sequenceA.
-
-#[global]
-Program Instance Traversable__UWord : Traversable GHC.Generics.UWord :=
-  fun _ k__ =>
-    k__ {| mapM__ := fun {m : Type -> Type}
-           {a : Type}
-           {b : Type}
-           `{GHC.Base.Monad m} =>
-             Traversable__UWord_mapM ;
-           sequence__ := fun {m : Type -> Type} {a : Type} `{GHC.Base.Monad m} =>
-             Traversable__UWord_sequence ;
-           sequenceA__ := fun {f : Type -> Type} {a : Type} `{GHC.Base.Applicative f} =>
-             Traversable__UWord_sequenceA ;
-           traverse__ := fun {f : Type -> Type}
-           {a : Type}
-           {b : Type}
-           `{GHC.Base.Applicative f} =>
-             Traversable__UWord_traverse |}.
-
-#[local] Definition Traversable__UInt_traverse
-   : forall {f : Type -> Type},
-     forall {a : Type},
-     forall {b : Type},
-     forall `{GHC.Base.Applicative f},
-     (a -> f b) -> GHC.Generics.UInt a -> f (GHC.Generics.UInt b) :=
-  fun {f : Type -> Type} {a : Type} {b : Type} `{GHC.Base.Applicative f} =>
-    fun arg_0__ arg_1__ =>
-      match arg_0__, arg_1__ with
-      | f, GHC.Generics.UInt a1 => GHC.Base.pure (GHC.Generics.UInt a1)
-      end.
-
-#[local] Definition Traversable__UInt_mapM
-   : forall {m : Type -> Type},
-     forall {a : Type},
-     forall {b : Type},
-     forall `{GHC.Base.Monad m},
-     (a -> m b) -> GHC.Generics.UInt a -> m (GHC.Generics.UInt b) :=
-  fun {m : Type -> Type} {a : Type} {b : Type} `{GHC.Base.Monad m} =>
-    Traversable__UInt_traverse.
-
-#[local] Definition Traversable__UInt_sequenceA
-   : forall {f : Type -> Type},
-     forall {a : Type},
-     forall `{GHC.Base.Applicative f},
-     GHC.Generics.UInt (f a) -> f (GHC.Generics.UInt a) :=
-  fun {f : Type -> Type} {a : Type} `{GHC.Base.Applicative f} =>
-    Traversable__UInt_traverse GHC.Base.id.
-
-#[local] Definition Traversable__UInt_sequence
-   : forall {m : Type -> Type},
-     forall {a : Type},
-     forall `{GHC.Base.Monad m},
-     GHC.Generics.UInt (m a) -> m (GHC.Generics.UInt a) :=
-  fun {m : Type -> Type} {a : Type} `{GHC.Base.Monad m} =>
-    Traversable__UInt_sequenceA.
-
-#[global]
-Program Instance Traversable__UInt : Traversable GHC.Generics.UInt :=
-  fun _ k__ =>
-    k__ {| mapM__ := fun {m : Type -> Type}
-           {a : Type}
-           {b : Type}
-           `{GHC.Base.Monad m} =>
-             Traversable__UInt_mapM ;
-           sequence__ := fun {m : Type -> Type} {a : Type} `{GHC.Base.Monad m} =>
-             Traversable__UInt_sequence ;
-           sequenceA__ := fun {f : Type -> Type} {a : Type} `{GHC.Base.Applicative f} =>
-             Traversable__UInt_sequenceA ;
-           traverse__ := fun {f : Type -> Type}
-           {a : Type}
-           {b : Type}
-           `{GHC.Base.Applicative f} =>
-             Traversable__UInt_traverse |}.
-
-#[local] Definition Traversable__UFloat_traverse
-   : forall {f : Type -> Type},
-     forall {a : Type},
-     forall {b : Type},
-     forall `{GHC.Base.Applicative f},
-     (a -> f b) -> GHC.Generics.UFloat a -> f (GHC.Generics.UFloat b) :=
-  fun {f : Type -> Type} {a : Type} {b : Type} `{GHC.Base.Applicative f} =>
-    fun arg_0__ arg_1__ =>
-      match arg_0__, arg_1__ with
-      | f, GHC.Generics.UFloat a1 => GHC.Base.pure (GHC.Generics.UFloat a1)
-      end.
-
-#[local] Definition Traversable__UFloat_mapM
-   : forall {m : Type -> Type},
-     forall {a : Type},
-     forall {b : Type},
-     forall `{GHC.Base.Monad m},
-     (a -> m b) -> GHC.Generics.UFloat a -> m (GHC.Generics.UFloat b) :=
-  fun {m : Type -> Type} {a : Type} {b : Type} `{GHC.Base.Monad m} =>
-    Traversable__UFloat_traverse.
-
-#[local] Definition Traversable__UFloat_sequenceA
-   : forall {f : Type -> Type},
-     forall {a : Type},
-     forall `{GHC.Base.Applicative f},
-     GHC.Generics.UFloat (f a) -> f (GHC.Generics.UFloat a) :=
-  fun {f : Type -> Type} {a : Type} `{GHC.Base.Applicative f} =>
-    Traversable__UFloat_traverse GHC.Base.id.
-
-#[local] Definition Traversable__UFloat_sequence
-   : forall {m : Type -> Type},
-     forall {a : Type},
-     forall `{GHC.Base.Monad m},
-     GHC.Generics.UFloat (m a) -> m (GHC.Generics.UFloat a) :=
-  fun {m : Type -> Type} {a : Type} `{GHC.Base.Monad m} =>
-    Traversable__UFloat_sequenceA.
-
-#[global]
-Program Instance Traversable__UFloat : Traversable GHC.Generics.UFloat :=
-  fun _ k__ =>
-    k__ {| mapM__ := fun {m : Type -> Type}
-           {a : Type}
-           {b : Type}
-           `{GHC.Base.Monad m} =>
-             Traversable__UFloat_mapM ;
-           sequence__ := fun {m : Type -> Type} {a : Type} `{GHC.Base.Monad m} =>
-             Traversable__UFloat_sequence ;
-           sequenceA__ := fun {f : Type -> Type} {a : Type} `{GHC.Base.Applicative f} =>
-             Traversable__UFloat_sequenceA ;
-           traverse__ := fun {f : Type -> Type}
-           {a : Type}
-           {b : Type}
-           `{GHC.Base.Applicative f} =>
-             Traversable__UFloat_traverse |}.
-
-#[local] Definition Traversable__UDouble_traverse
-   : forall {f : Type -> Type},
-     forall {a : Type},
-     forall {b : Type},
-     forall `{GHC.Base.Applicative f},
-     (a -> f b) -> GHC.Generics.UDouble a -> f (GHC.Generics.UDouble b) :=
-  fun {f : Type -> Type} {a : Type} {b : Type} `{GHC.Base.Applicative f} =>
-    fun arg_0__ arg_1__ =>
-      match arg_0__, arg_1__ with
-      | f, GHC.Generics.UDouble a1 => GHC.Base.pure (GHC.Generics.UDouble a1)
-      end.
-
-#[local] Definition Traversable__UDouble_mapM
-   : forall {m : Type -> Type},
-     forall {a : Type},
-     forall {b : Type},
-     forall `{GHC.Base.Monad m},
-     (a -> m b) -> GHC.Generics.UDouble a -> m (GHC.Generics.UDouble b) :=
-  fun {m : Type -> Type} {a : Type} {b : Type} `{GHC.Base.Monad m} =>
-    Traversable__UDouble_traverse.
-
-#[local] Definition Traversable__UDouble_sequenceA
-   : forall {f : Type -> Type},
-     forall {a : Type},
-     forall `{GHC.Base.Applicative f},
-     GHC.Generics.UDouble (f a) -> f (GHC.Generics.UDouble a) :=
-  fun {f : Type -> Type} {a : Type} `{GHC.Base.Applicative f} =>
-    Traversable__UDouble_traverse GHC.Base.id.
-
-#[local] Definition Traversable__UDouble_sequence
-   : forall {m : Type -> Type},
-     forall {a : Type},
-     forall `{GHC.Base.Monad m},
-     GHC.Generics.UDouble (m a) -> m (GHC.Generics.UDouble a) :=
-  fun {m : Type -> Type} {a : Type} `{GHC.Base.Monad m} =>
-    Traversable__UDouble_sequenceA.
-
-#[global]
-Program Instance Traversable__UDouble : Traversable GHC.Generics.UDouble :=
-  fun _ k__ =>
-    k__ {| mapM__ := fun {m : Type -> Type}
-           {a : Type}
-           {b : Type}
-           `{GHC.Base.Monad m} =>
-             Traversable__UDouble_mapM ;
-           sequence__ := fun {m : Type -> Type} {a : Type} `{GHC.Base.Monad m} =>
-             Traversable__UDouble_sequence ;
-           sequenceA__ := fun {f : Type -> Type} {a : Type} `{GHC.Base.Applicative f} =>
-             Traversable__UDouble_sequenceA ;
-           traverse__ := fun {f : Type -> Type}
-           {a : Type}
-           {b : Type}
-           `{GHC.Base.Applicative f} =>
-             Traversable__UDouble_traverse |}.
-
-#[local] Definition Traversable__UChar_traverse
-   : forall {f : Type -> Type},
-     forall {a : Type},
-     forall {b : Type},
-     forall `{GHC.Base.Applicative f},
-     (a -> f b) -> GHC.Generics.UChar a -> f (GHC.Generics.UChar b) :=
-  fun {f : Type -> Type} {a : Type} {b : Type} `{GHC.Base.Applicative f} =>
-    fun arg_0__ arg_1__ =>
-      match arg_0__, arg_1__ with
-      | f, GHC.Generics.UChar a1 => GHC.Base.pure (GHC.Generics.UChar a1)
-      end.
-
-#[local] Definition Traversable__UChar_mapM
-   : forall {m : Type -> Type},
-     forall {a : Type},
-     forall {b : Type},
-     forall `{GHC.Base.Monad m},
-     (a -> m b) -> GHC.Generics.UChar a -> m (GHC.Generics.UChar b) :=
-  fun {m : Type -> Type} {a : Type} {b : Type} `{GHC.Base.Monad m} =>
-    Traversable__UChar_traverse.
-
-#[local] Definition Traversable__UChar_sequenceA
-   : forall {f : Type -> Type},
-     forall {a : Type},
-     forall `{GHC.Base.Applicative f},
-     GHC.Generics.UChar (f a) -> f (GHC.Generics.UChar a) :=
-  fun {f : Type -> Type} {a : Type} `{GHC.Base.Applicative f} =>
-    Traversable__UChar_traverse GHC.Base.id.
-
-#[local] Definition Traversable__UChar_sequence
-   : forall {m : Type -> Type},
-     forall {a : Type},
-     forall `{GHC.Base.Monad m},
-     GHC.Generics.UChar (m a) -> m (GHC.Generics.UChar a) :=
-  fun {m : Type -> Type} {a : Type} `{GHC.Base.Monad m} =>
-    Traversable__UChar_sequenceA.
-
-#[global]
-Program Instance Traversable__UChar : Traversable GHC.Generics.UChar :=
-  fun _ k__ =>
-    k__ {| mapM__ := fun {m : Type -> Type}
-           {a : Type}
-           {b : Type}
-           `{GHC.Base.Monad m} =>
-             Traversable__UChar_mapM ;
-           sequence__ := fun {m : Type -> Type} {a : Type} `{GHC.Base.Monad m} =>
-             Traversable__UChar_sequence ;
-           sequenceA__ := fun {f : Type -> Type} {a : Type} `{GHC.Base.Applicative f} =>
-             Traversable__UChar_sequenceA ;
-           traverse__ := fun {f : Type -> Type}
-           {a : Type}
-           {b : Type}
-           `{GHC.Base.Applicative f} =>
-             Traversable__UChar_traverse |}.
+(* Skipping instance `Data.Traversable.Traversable__UWord' of class
+   `Data.Traversable.Traversable' *)
 
-#[local] Definition Traversable__UAddr_traverse
-   : forall {f : Type -> Type},
-     forall {a : Type},
-     forall {b : Type},
-     forall `{GHC.Base.Applicative f},
-     (a -> f b) -> GHC.Generics.UAddr a -> f (GHC.Generics.UAddr b) :=
-  fun {f : Type -> Type} {a : Type} {b : Type} `{GHC.Base.Applicative f} =>
-    fun arg_0__ arg_1__ =>
-      match arg_0__, arg_1__ with
-      | f, GHC.Generics.UAddr a1 => GHC.Base.pure (GHC.Generics.UAddr a1)
-      end.
+(* Skipping instance `Data.Traversable.Traversable__UInt' of class
+   `Data.Traversable.Traversable' *)
 
-#[local] Definition Traversable__UAddr_mapM
-   : forall {m : Type -> Type},
-     forall {a : Type},
-     forall {b : Type},
-     forall `{GHC.Base.Monad m},
-     (a -> m b) -> GHC.Generics.UAddr a -> m (GHC.Generics.UAddr b) :=
-  fun {m : Type -> Type} {a : Type} {b : Type} `{GHC.Base.Monad m} =>
-    Traversable__UAddr_traverse.
+(* Skipping instance `Data.Traversable.Traversable__UFloat' of class
+   `Data.Traversable.Traversable' *)
 
-#[local] Definition Traversable__UAddr_sequenceA
-   : forall {f : Type -> Type},
-     forall {a : Type},
-     forall `{GHC.Base.Applicative f},
-     GHC.Generics.UAddr (f a) -> f (GHC.Generics.UAddr a) :=
-  fun {f : Type -> Type} {a : Type} `{GHC.Base.Applicative f} =>
-    Traversable__UAddr_traverse GHC.Base.id.
+(* Skipping instance `Data.Traversable.Traversable__UDouble' of class
+   `Data.Traversable.Traversable' *)
 
-#[local] Definition Traversable__UAddr_sequence
-   : forall {m : Type -> Type},
-     forall {a : Type},
-     forall `{GHC.Base.Monad m},
-     GHC.Generics.UAddr (m a) -> m (GHC.Generics.UAddr a) :=
-  fun {m : Type -> Type} {a : Type} `{GHC.Base.Monad m} =>
-    Traversable__UAddr_sequenceA.
+(* Skipping instance `Data.Traversable.Traversable__UChar' of class
+   `Data.Traversable.Traversable' *)
 
-#[global]
-Program Instance Traversable__UAddr : Traversable GHC.Generics.UAddr :=
-  fun _ k__ =>
-    k__ {| mapM__ := fun {m : Type -> Type}
-           {a : Type}
-           {b : Type}
-           `{GHC.Base.Monad m} =>
-             Traversable__UAddr_mapM ;
-           sequence__ := fun {m : Type -> Type} {a : Type} `{GHC.Base.Monad m} =>
-             Traversable__UAddr_sequence ;
-           sequenceA__ := fun {f : Type -> Type} {a : Type} `{GHC.Base.Applicative f} =>
-             Traversable__UAddr_sequenceA ;
-           traverse__ := fun {f : Type -> Type}
-           {a : Type}
-           {b : Type}
-           `{GHC.Base.Applicative f} =>
-             Traversable__UAddr_traverse |}.
+(* Skipping instance `Data.Traversable.Traversable__UAddr' of class
+   `Data.Traversable.Traversable' *)
 
 (* Skipping instance `Data.Traversable.Traversable__op_ZCziZC__' of class
    `Data.Traversable.Traversable' *)
@@ -484,45 +172,37 @@ Program Instance Traversable__UAddr : Traversable GHC.Generics.UAddr :=
    : forall {f : Type -> Type},
      forall {a : Type},
      forall {b : Type},
-     forall `{GHC.Base.Applicative f},
-     (a -> f b) ->
-     Data.Functor.Identity.Identity a -> f (Data.Functor.Identity.Identity b) :=
+     forall `{GHC.Base.Applicative f}, (a -> f b) -> Identity a -> f (Identity b) :=
   fun {f : Type -> Type} {a : Type} {b : Type} `{GHC.Base.Applicative f} =>
     fun arg_0__ arg_1__ =>
       match arg_0__, arg_1__ with
-      | f, Data.Functor.Identity.Mk_Identity a1 =>
-          GHC.Base.fmap (fun b1 => Data.Functor.Identity.Mk_Identity b1) (f a1)
+      | f, Mk_Identity a1 => GHC.Base.fmap (fun b1 => Mk_Identity b1) (f a1)
       end.
 
 #[local] Definition Traversable__Identity_mapM
    : forall {m : Type -> Type},
      forall {a : Type},
      forall {b : Type},
-     forall `{GHC.Base.Monad m},
-     (a -> m b) ->
-     Data.Functor.Identity.Identity a -> m (Data.Functor.Identity.Identity b) :=
+     forall `{GHC.Base.Monad m}, (a -> m b) -> Identity a -> m (Identity b) :=
   fun {m : Type -> Type} {a : Type} {b : Type} `{GHC.Base.Monad m} =>
     Traversable__Identity_traverse.
 
 #[local] Definition Traversable__Identity_sequenceA
    : forall {f : Type -> Type},
      forall {a : Type},
-     forall `{GHC.Base.Applicative f},
-     Data.Functor.Identity.Identity (f a) -> f (Data.Functor.Identity.Identity a) :=
+     forall `{GHC.Base.Applicative f}, Identity (f a) -> f (Identity a) :=
   fun {f : Type -> Type} {a : Type} `{GHC.Base.Applicative f} =>
     Traversable__Identity_traverse GHC.Base.id.
 
 #[local] Definition Traversable__Identity_sequence
    : forall {m : Type -> Type},
      forall {a : Type},
-     forall `{GHC.Base.Monad m},
-     Data.Functor.Identity.Identity (m a) -> m (Data.Functor.Identity.Identity a) :=
+     forall `{GHC.Base.Monad m}, Identity (m a) -> m (Identity a) :=
   fun {m : Type -> Type} {a : Type} `{GHC.Base.Monad m} =>
     Traversable__Identity_sequenceA.
 
 #[global]
-Program Instance Traversable__Identity
-   : Traversable Data.Functor.Identity.Identity :=
+Program Instance Traversable__Identity : Traversable Identity :=
   fun _ k__ =>
     k__ {| mapM__ := fun {m : Type -> Type}
            {a : Type}
@@ -1265,16 +945,14 @@ Program Instance Traversable__Ap {f : Type -> Type} `{(Traversable f)}
 #[global] Definition fmapDefault {t : Type -> Type} {a : Type} {b : Type}
   `{Traversable t}
    : (a -> b) -> t a -> t b :=
-  GHC.Prim.coerce (traverse : (a -> Data.Functor.Identity.Identity b) ->
-                   t a -> Data.Functor.Identity.Identity (t b)).
+  GHC.Prim.coerce (traverse : (a -> Identity b) -> t a -> Identity (t b)).
 
 (* Skipping definition `Data.Traversable.foldMapDefault' *)
 
 (* External variables:
-     None Some Type cons list nil op_zt__ option pair Data.Either.Either
-     Data.Either.Left Data.Either.Right Data.Foldable.Foldable
+     Identity Mk_Identity None Some Type cons list nil op_zt__ option pair
+     Data.Either.Either Data.Either.Left Data.Either.Right Data.Foldable.Foldable
      Data.Functor.op_zlzdzg__ Data.Functor.Const.Const Data.Functor.Const.Mk_Const
-     Data.Functor.Identity.Identity Data.Functor.Identity.Mk_Identity
      Data.Functor.Utils.Mk_StateL Data.Functor.Utils.Mk_StateR
      Data.Functor.Utils.runStateL Data.Functor.Utils.runStateR Data.Monoid.Ap
      Data.Monoid.Mk_Ap Data.Ord.Down Data.Ord.Mk_Down Data.Proxy.Mk_Proxy
@@ -1284,7 +962,5 @@ Program Instance Traversable__Ap {f : Type -> Type} `{(Traversable f)}
      Data.SemigroupInternal.Product Data.SemigroupInternal.Sum GHC.Base.Applicative
      GHC.Base.Functor GHC.Base.Monad GHC.Base.NEcons GHC.Base.NonEmpty GHC.Base.flip
      GHC.Base.fmap GHC.Base.foldr GHC.Base.id GHC.Base.liftA2 GHC.Base.op_z2218U__
-     GHC.Base.pure GHC.Generics.UAddr GHC.Generics.UChar GHC.Generics.UDouble
-     GHC.Generics.UFloat GHC.Generics.UInt GHC.Generics.UWord GHC.Prim.coerce
-     GHC.Tuple.pair2 GHC.Tuple.pair_type
+     GHC.Base.pure GHC.Prim.coerce GHC.Tuple.pair2 GHC.Tuple.pair_type
 *)
diff --git a/base/Data/Void.v b/base/Data/Void.v
index aaf7752d..4292d495 100644
--- a/base/Data/Void.v
+++ b/base/Data/Void.v
@@ -13,6 +13,7 @@ Require Coq.Program.Wf.
 (* Converted imports: *)
 
 Require GHC.Base.
+Import GHC.Base.Notations.
 
 (* Converted type declarations: *)
 
@@ -20,6 +21,62 @@ Inductive Void : Type :=.
 
 (* Converted value declarations: *)
 
+#[local] Definition Eq___Void_op_zeze__ : Void -> Void -> bool :=
+  fun arg_0__ arg_1__ => match arg_0__, arg_1__ with | _, z => true end.
+
+#[local] Definition Eq___Void_op_zsze__ : Void -> Void -> bool :=
+  fun x y => negb (Eq___Void_op_zeze__ x y).
+
+#[global]
+Program Instance Eq___Void : GHC.Base.Eq_ Void :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zeze____ := Eq___Void_op_zeze__ ;
+           GHC.Base.op_zsze____ := Eq___Void_op_zsze__ |}.
+
+(* Skipping all instances of class `Data.Data.Data', including
+   `Data.Void.Data__Void' *)
+
+(* Skipping all instances of class `GHC.Generics.Generic', including
+   `Data.Void.Generic__Void' *)
+
+#[local] Definition Ord__Void_compare : Void -> Void -> comparison :=
+  fun arg_0__ arg_1__ => match arg_0__, arg_1__ with | _, z => Eq end.
+
+#[local] Definition Ord__Void_op_zl__ : Void -> Void -> bool :=
+  fun x y => Ord__Void_compare x y GHC.Base.== Lt.
+
+#[local] Definition Ord__Void_op_zlze__ : Void -> Void -> bool :=
+  fun x y => Ord__Void_compare x y GHC.Base./= Gt.
+
+#[local] Definition Ord__Void_op_zg__ : Void -> Void -> bool :=
+  fun x y => Ord__Void_compare x y GHC.Base.== Gt.
+
+#[local] Definition Ord__Void_op_zgze__ : Void -> Void -> bool :=
+  fun x y => Ord__Void_compare x y GHC.Base./= Lt.
+
+#[local] Definition Ord__Void_max : Void -> Void -> Void :=
+  fun x y => if Ord__Void_op_zlze__ x y : bool then y else x.
+
+#[local] Definition Ord__Void_min : Void -> Void -> Void :=
+  fun x y => if Ord__Void_op_zlze__ x y : bool then x else y.
+
+#[global]
+Program Instance Ord__Void : GHC.Base.Ord Void :=
+  fun _ k__ =>
+    k__ {| GHC.Base.op_zl____ := Ord__Void_op_zl__ ;
+           GHC.Base.op_zlze____ := Ord__Void_op_zlze__ ;
+           GHC.Base.op_zg____ := Ord__Void_op_zg__ ;
+           GHC.Base.op_zgze____ := Ord__Void_op_zgze__ ;
+           GHC.Base.compare__ := Ord__Void_compare ;
+           GHC.Base.max__ := Ord__Void_max ;
+           GHC.Base.min__ := Ord__Void_min |}.
+
+(* Skipping all instances of class `GHC.Read.Read', including
+   `Data.Void.Read__Void' *)
+
+(* Skipping all instances of class `GHC.Show.Show', including
+   `Data.Void.Show__Void' *)
+
 (* Skipping all instances of class `GHC.Ix.Ix', including
    `Data.Void.Ix__Void' *)
 
@@ -42,5 +99,9 @@ Program Instance Semigroup__Void : GHC.Base.Semigroup Void :=
   GHC.Base.fmap absurd.
 
 (* External variables:
-     Type GHC.Base.Functor GHC.Base.Semigroup GHC.Base.fmap GHC.Base.op_zlzlzgzg____
+     Eq Gt Lt Type bool comparison negb true GHC.Base.Eq_ GHC.Base.Functor
+     GHC.Base.Ord GHC.Base.Semigroup GHC.Base.compare__ GHC.Base.fmap GHC.Base.max__
+     GHC.Base.min__ GHC.Base.op_zeze__ GHC.Base.op_zeze____ GHC.Base.op_zg____
+     GHC.Base.op_zgze____ GHC.Base.op_zl____ GHC.Base.op_zlze____
+     GHC.Base.op_zlzlzgzg____ GHC.Base.op_zsze__ GHC.Base.op_zsze____
 *)
diff --git a/base/GHC/Base.v b/base/GHC/Base.v
index 1b29df1f..c03d4241 100644
--- a/base/GHC/Base.v
+++ b/base/GHC/Base.v
@@ -10,6 +10,9 @@ Unset Printing Implicit Defensive.
 Require Coq.Program.Tactics.
 Require Coq.Program.Wf.
 
+(* Preamble *)
+
+
 (* Converted imports: *)
 
 Require Coq.Init.Datatypes.
@@ -577,6 +580,91 @@ End ManualNotations.
 
 (* Converted value declarations: *)
 
+#[local] Definition Eq___option_op_zeze__ {inst_a : Type} `{Eq_ inst_a}
+   : option inst_a -> option inst_a -> bool :=
+  fun arg_0__ arg_1__ =>
+    match arg_0__, arg_1__ with
+    | None, None => true
+    | Some a1, Some b1 => ((a1 == b1))
+    | _, _ => false
+    end.
+
+#[local] Definition Eq___option_op_zsze__ {inst_a : Type} `{Eq_ inst_a}
+   : option inst_a -> option inst_a -> bool :=
+  fun x y => negb (Eq___option_op_zeze__ x y).
+
+#[global]
+Program Instance Eq___option {a : Type} `{Eq_ a} : Eq_ (option a) :=
+  fun _ k__ =>
+    k__ {| op_zeze____ := Eq___option_op_zeze__ ;
+           op_zsze____ := Eq___option_op_zsze__ |}.
+
+#[local] Definition Ord__option_op_zl__ {inst_a : Type} `{Ord inst_a}
+   : option inst_a -> option inst_a -> bool :=
+  fun a b =>
+    match a with
+    | None => match b with | None => false | _ => true end
+    | Some a1 => match b with | Some b1 => (a1 < b1) | _ => false end
+    end.
+
+#[local] Definition Ord__option_op_zlze__ {inst_a : Type} `{Ord inst_a}
+   : option inst_a -> option inst_a -> bool :=
+  fun a b => negb (Ord__option_op_zl__ b a).
+
+#[local] Definition Ord__option_op_zg__ {inst_a : Type} `{Ord inst_a}
+   : option inst_a -> option inst_a -> bool :=
+  fun a b => Ord__option_op_zl__ b a.
+
+#[local] Definition Ord__option_op_zgze__ {inst_a : Type} `{Ord inst_a}
+   : option inst_a -> option inst_a -> bool :=
+  fun a b => negb (Ord__option_op_zl__ a b).
+
+#[local] Definition Ord__option_compare {inst_a : Type} `{Ord inst_a}
+   : option inst_a -> option inst_a -> comparison :=
+  fun a b =>
+    match a with
+    | None => match b with | None => Eq | _ => Lt end
+    | Some a1 => match b with | Some b1 => (compare a1 b1) | _ => Gt end
+    end.
+
+#[local] Definition Ord__option_max {inst_a : Type} `{Ord inst_a}
+   : option inst_a -> option inst_a -> option inst_a :=
+  fun x y => if Ord__option_op_zlze__ x y : bool then y else x.
+
+#[local] Definition Ord__option_min {inst_a : Type} `{Ord inst_a}
+   : option inst_a -> option inst_a -> option inst_a :=
+  fun x y => if Ord__option_op_zlze__ x y : bool then x else y.
+
+#[global]
+Program Instance Ord__option {a : Type} `{Ord a} : Ord (option a) :=
+  fun _ k__ =>
+    k__ {| op_zl____ := Ord__option_op_zl__ ;
+           op_zlze____ := Ord__option_op_zlze__ ;
+           op_zg____ := Ord__option_op_zg__ ;
+           op_zgze____ := Ord__option_op_zgze__ ;
+           compare__ := Ord__option_compare ;
+           max__ := Ord__option_max ;
+           min__ := Ord__option_min |}.
+
+#[local] Definition Eq___NonEmpty_op_zeze__ {inst_a : Type} `{Eq_ inst_a}
+   : NonEmpty inst_a -> NonEmpty inst_a -> bool :=
+  fun arg_0__ arg_1__ =>
+    match arg_0__, arg_1__ with
+    | NEcons a1 a2, NEcons b1 b2 => (andb ((a1 == b1)) ((a2 == b2)))
+    end.
+
+#[local] Definition Eq___NonEmpty_op_zsze__ {inst_a : Type} `{Eq_ inst_a}
+   : NonEmpty inst_a -> NonEmpty inst_a -> bool :=
+  fun x y => negb (Eq___NonEmpty_op_zeze__ x y).
+
+#[global]
+Program Instance Eq___NonEmpty {a : Type} `{Eq_ a} : Eq_ (NonEmpty a) :=
+  fun _ k__ =>
+    k__ {| op_zeze____ := Eq___NonEmpty_op_zeze__ ;
+           op_zsze____ := Eq___NonEmpty_op_zsze__ |}.
+
+(* Skipping instance `GHC.Base.Ord__NonEmpty' of class `GHC.Base.Ord' *)
+
 #[local] Definition Semigroup__list_op_zlzlzgzg__ {inst_a : Type}
    : list inst_a -> list inst_a -> list inst_a :=
   Coq.Init.Datatypes.app.
@@ -1610,22 +1698,12 @@ Fixpoint eqString (arg_0__ arg_1__ : String) : bool
    : (a -> b -> c) -> b -> a -> c :=
   fun f x y => f y x.
 
-#[global] Definition op_zd__ {r : GHC.Types.RuntimeRep} {a : Type} {b : Type}
-   : (a -> b) -> a -> b :=
+#[global] Definition op_zd__ {a} {b} : (a -> b) -> a -> b :=
   fun f x => f x.
 
-Notation "'_$_'" := (op_zd__).
-
-Infix "$" := (_$_) (at level 99).
-
-#[global] Definition op_zdzn__ {r : GHC.Types.RuntimeRep} {a : Type} {b : Type}
-   : (a -> b) -> a -> b :=
+#[global] Definition op_zdzn__ {a : Type} {b : Type} : (a -> b) -> a -> b :=
   fun f x => let vx := x in f vx.
 
-Notation "'_$!_'" := (op_zdzn__).
-
-Infix "$!" := (_$!_) (at level 99).
-
 (* Skipping definition `GHC.Base.until' *)
 
 #[global] Definition asTypeOf {a : Type} : a -> a -> a :=
@@ -1687,15 +1765,12 @@ Notation "'_GHC.Base.<**>_'" := (op_zlztztzg__).
 Infix "GHC.Base.<**>" := (_<**>_) (at level 99).
 Notation "'_GHC.Base.=<<_'" := (op_zezlzl__).
 Infix "GHC.Base.=<<" := (_=<<_) (at level 99).
-Notation "'_GHC.Base.$_'" := (op_zd__).
-Infix "GHC.Base.$" := (_$_) (at level 99).
-Notation "'_GHC.Base.$!_'" := (op_zdzn__).
-Infix "GHC.Base.$!" := (_$!_) (at level 99).
 End Notations.
 
 (* External variables:
-     Eq Gt Lt None Some String Type andb bool comparison cons false list nil
-     op_zeze__ option pair true tt unit Coq.Init.Datatypes.app
-     Coq.Lists.List.flat_map Coq.Lists.List.map GHC.Prim.arrow GHC.Tuple.pair_type
-     GHC.Tuple.quad_type GHC.Tuple.triple_type GHC.Types.RuntimeRep
+     Eq Eq_ Gt Lt None Ord Some String Type andb bool compare compare__ comparison
+     cons false list max__ min__ negb nil op_zeze__ op_zeze____ op_zg____ op_zgze____
+     op_zl__ op_zl____ op_zlze____ op_zsze____ option pair true tt unit
+     Coq.Init.Datatypes.app Coq.Lists.List.flat_map Coq.Lists.List.map GHC.Prim.arrow
+     GHC.Tuple.pair_type GHC.Tuple.quad_type GHC.Tuple.triple_type
 *)
diff --git a/base/_CoqProject b/base/_CoqProject
index 518ce675..6ca16770 100644
--- a/base/_CoqProject
+++ b/base/_CoqProject
@@ -1,6 +1,6 @@
 -Q . ""
 HsToCoq/Wf.v HsToCoq/Skip.v HsToCoq/DeferredFix.v HsToCoq/DeferredFixImpl.v HsToCoq/Unpeel.v GHC/Num.v GHC/Char.v GHC/Real.v GHC/Enum.v Data/Bits.v GHC/Prim.v GHC/Types.v GHC/Tuple.v Data/Type/Equality.v HsToCoq/Err.v GHC/Err.v HsToCoq/Nat.v GHC/Unicode.v Prelude.v
-GHC/Base.v Data/Maybe.v GHC/List.v Data/List.v Data/OldList.v Data/Bool.v Data/Tuple.v Data/Void.v Data/Function.v Data/Ord.v Data/Functor.v Data/Either.v Data/Proxy.v Control/Monad.v Data/Monoid.v Data/Functor/Utils.v Data/Traversable.v Control/Monad/Fail.v Data/Foldable.v Control/Arrow.v Data/Functor/Identity.v Data/Functor/Const.v Control/Applicative.v Data/Functor/Classes.v Control/Category.v Data/Bifunctor.v Data/List/NonEmpty.v Data/Semigroup.v Data/Functor/Compose.v Data/Functor/Product.v Data/Functor/Sum.v Data/Bifoldable.v Data/Bitraversable.v Control/Monad/Zip.v
+Data/Maybe.v GHC/List.v Data/List.v Data/OldList.v Data/Bool.v Data/Tuple.v Data/Void.v Data/Function.v Data/Ord.v Data/Functor.v Data/Either.v Data/Proxy.v Control/Monad.v Data/Monoid.v Data/Functor/Utils.v Data/Traversable.v Control/Monad/Fail.v Data/Foldable.v Control/Arrow.v Data/Functor/Identity.v Data/Functor/Const.v Control/Applicative.v Data/Functor/Classes.v Control/Category.v Data/Bifunctor.v Data/List/NonEmpty.v Data/Semigroup.v Data/Functor/Compose.v Data/Functor/Product.v Data/Functor/Sum.v Data/Bifoldable.v Data/Bitraversable.v Control/Monad/Zip.v
 Data/SemigroupInternal.v
-
+GHC/Base.v