diff --git a/FiniteSets/_CoqProject b/FiniteSets/_CoqProject
index 2798969..c862751 100644
--- a/FiniteSets/_CoqProject
+++ b/FiniteSets/_CoqProject
@@ -1,6 +1,7 @@
 -R . "" COQC = hoqc COQDEP = hoqdep
 -R ../prelude ""
 notation.v
+plumbing.v
 lattice.v
 disjunction.v
 representations/bad.v
diff --git a/FiniteSets/plumbing.v b/FiniteSets/plumbing.v
new file mode 100644
index 0000000..f187584
--- /dev/null
+++ b/FiniteSets/plumbing.v
@@ -0,0 +1,16 @@
+Require Import HoTT.
+
+(* Lemmas from this file do not belong in this project. *)
+(* Some of them should probably be in the HoTT library? *)
+
+Lemma ap_inl_path_sum_inl {A B} (x y : A) (p : inl x = inl y) :
+  ap inl (path_sum_inl B p) = p.
+Proof.
+  transitivity (@path_sum _ B (inl x) (inl y) (path_sum_inl B p));
+    [ | apply (eisretr_path_sum _) ].
+  destruct (path_sum_inl B p).
+  reflexivity.
+Defined.
+Lemma ap_equiv {A B} (f : A <~> B) {x y : A} (p : x = y) :
+  ap (f^-1 o f) p = eissect f x @ p @ (eissect f y)^.
+Proof. destruct p. hott_simpl. Defined.
diff --git a/FiniteSets/variations/b_finite.v b/FiniteSets/variations/b_finite.v
index 66c9a8c..b321059 100644
--- a/FiniteSets/variations/b_finite.v
+++ b/FiniteSets/variations/b_finite.v
@@ -1,5 +1,5 @@
 (* Bishop-finiteness is that "default" notion of finiteness in the HoTT library *)
-Require Import HoTT HitTactics.
+Require Import HoTT HitTactics plumbing.
 Require Import Sub notation variations.k_finite.
 Require Import fsets.properties.
 
@@ -150,21 +150,6 @@ Section empty.
   Defined.  
 End empty.
 
-
-(* TODO: This should go into the HoTT library or in some other places *)
-Lemma ap_inl_path_sum_inl {A B} (x y : A) (p : inl x = inl y) :
-  ap inl (path_sum_inl B p) = p.
-Proof.
-  transitivity (@path_sum _ B (inl x) (inl y) (path_sum_inl B p));
-    [ | apply (eisretr_path_sum _) ].
-  destruct (path_sum_inl B p).
-  reflexivity.
-Defined.
-Lemma ap_equiv {A B} (f : A <~> B) {x y : A} (p : x = y) :
-  ap (f^-1 o f) p = eissect f x @ p @ (eissect f y)^.
-Proof. destruct p. hott_simpl. Defined.
-(* END TODO *)
-
 Section split.
   Context `{Univalence}.
   Variable (A : Type).