diff --git a/src/Control/Monad/Indexed.v b/src/Control/Monad/Indexed.v
index 6722a4c..be6447e 100644
--- a/src/Control/Monad/Indexed.v
+++ b/src/Control/Monad/Indexed.v
@@ -1,5 +1,6 @@
 Require Import Hask.Ltac.
 Require Import Hask.Prelude.
+Require Import FunctionalExtensionality.
 
 Generalizable All Variables.
 Set Primitive Projections.
@@ -126,8 +127,6 @@ Ltac rewrite_iapp_homomorphisms :=
 
 Section IApplicatives.
 
-  Require Import FunctionalExtensionality.
-
   Variable F : Type -> Type -> Type -> Type.
   Context `{IApplicative F}.
 
diff --git a/src/Haskell.v b/src/Haskell.v
index 62743fa..86f8ba7 100644
--- a/src/Haskell.v
+++ b/src/Haskell.v
@@ -63,10 +63,10 @@ Extract Inlined Constant projT1    => "Prelude.fst".
 Extract Inlined Constant snd       => "Prelude.snd".
 (* Extract Inlined Constant subn      => "(Prelude.-)". *)
 
-Extraction Implicit eq_rect [ x y ].
-Extraction Implicit eq_rect_r [ x y ].
-Extraction Implicit eq_rec [ x y ].
-Extraction Implicit eq_rec_r [ x y ].
+(* Extraction Implicit eq_rect [ x y ]. *)
+(* Extraction Implicit eq_rect_r [ x y ]. *)
+(* Extraction Implicit eq_rec [ x y ]. *)
+(* Extraction Implicit eq_rec_r [ x y ]. *)
 
 Extract Inlined Constant eq_rect => "".
 Extract Inlined Constant eq_rect_r => "".