From b17a726608dca1c9cdc71a9973f52b3c53532b6d Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Thu, 24 Aug 2017 18:41:31 +0200
Subject: [PATCH] A simple proof that Bfin implies Kfin

---
 FiniteSets/variations/b_finite.v | 23 +++++++++++++++++++++--
 1 file changed, 21 insertions(+), 2 deletions(-)

diff --git a/FiniteSets/variations/b_finite.v b/FiniteSets/variations/b_finite.v
index b321059..d9710d3 100644
--- a/FiniteSets/variations/b_finite.v
+++ b/FiniteSets/variations/b_finite.v
@@ -310,9 +310,28 @@ Section dec_membership.
 End dec_membership.
 
 Section bfin_kfin.
-  Variable (A : Type).
   Context `{Univalence}.
-  Definition bfin_to_kfin : forall (P : Sub A), Bfin P -> Kf_sub _ P.
+  Lemma bfin_to_kfin : forall (B : Type), Finite B -> Kf B.
+  Proof.
+    apply finite_ind_hprop.
+    - intros. apply _.
+    - apply Kf_unfold.
+      exists ∅. intros [].
+    - intros B [n f] IH.
+      strip_truncations.
+      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.
+        apply fmap_isIn.
+        apply (HX a).
+      + right. apply (tr idpath).
+  Defined.
+
+  Definition bfin_to_kfin_sub A : forall (P : Sub A), Bfin P -> Kf_sub _ P.
   Proof.
     intros P [n f].
     strip_truncations.