From e8560a0c071efa32d490d92a88a15e3543021704 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Thu, 24 Aug 2017 18:52:43 +0200
Subject: [PATCH] tfw importin the middle of the file

---
 FiniteSets/variations/b_finite.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/FiniteSets/variations/b_finite.v b/FiniteSets/variations/b_finite.v
index d9710d3..811aa64 100644
--- a/FiniteSets/variations/b_finite.v
+++ b/FiniteSets/variations/b_finite.v
@@ -1,7 +1,7 @@
 (* Bishop-finiteness is that "default" notion of finiteness in the HoTT library *)
 Require Import HoTT HitTactics plumbing.
 Require Import Sub notation variations.k_finite.
-Require Import fsets.properties.
+Require Import fsets.properties fsets.monad.
 
 Section finite_hott.
   Variable (A : Type).
@@ -322,7 +322,6 @@ Section bfin_kfin.
       apply Kf_unfold in IH.
       destruct IH as [X HX].
       apply Kf_unfold.
-      Require Import fsets.monad.
       exists ((ffmap inl X) ∪ {|inr tt|}); simpl.
       intros [a | []]; apply tr.
       + left.