diff --git a/_CoqProject b/_CoqProject
index 1a54a3ca2a3c98693c7a17446eaa7bc8590c067f..0f233d111c04b9920d516bb407a523eee733c31f 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -49,7 +49,7 @@ algebra/agree.v
 algebra/excl.v
 algebra/iprod.v
 algebra/functor.v
-program_logic/upred.v
+algebra/upred.v
 program_logic/model.v
 program_logic/adequacy.v
 program_logic/hoare_lifting.v
diff --git a/program_logic/upred.v b/algebra/upred.v
similarity index 100%
rename from program_logic/upred.v
rename to algebra/upred.v
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index b60a5fba156987ff5b54d88d3676fcc15ae073cb..572d95cc396d9e9b3ab4b5283a10a3f48986faf6 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -1,5 +1,5 @@
 (** This file is essentially a bunch of testcases. *)
-Require Import program_logic.upred program_logic.ownership.
+Require Import program_logic.ownership.
 Require Import heap_lang.lifting heap_lang.sugar.
 Import heap_lang uPred notations.
 
diff --git a/prelude/co_pset.v b/prelude/co_pset.v
index 7516f56cda8f9971b0d052a15e15bf267ff20c56..3b49cb373059d3d8b1c1dda5aee2b73e14af5587 100644
--- a/prelude/co_pset.v
+++ b/prelude/co_pset.v
@@ -331,12 +331,11 @@ Proof.
       rewrite ?coPset_elem_of_node; naive_solver.
   * by intros [q' ->]; induction q; simpl; rewrite ?coPset_elem_of_node.
 Qed.
-
 Lemma coPset_suffixes_infinite p : ¬set_finite (coPset_suffixes p).
 Proof.
   rewrite coPset_finite_spec; simpl.
-  (* FIXME no time to finish right now, but I think it holds *)
-Abort. 
+  induction p; simpl; rewrite ?coPset_finite_node, ?andb_True; naive_solver.
+Qed.
 
 (** * Splitting of infinite sets *)
 Fixpoint coPset_l_raw (t : coPset_raw) : coPset_raw :=
diff --git a/program_logic/model.v b/program_logic/model.v
index a64a8c579309b65f977fc4d13b3b9baf6bcb22e9..ca0bbec0cac4abb1240ddf7796088f1eb49c5a79 100644
--- a/program_logic/model.v
+++ b/program_logic/model.v
@@ -1,4 +1,4 @@
-Require Export program_logic.upred program_logic.resources.
+Require Export algebra.upred program_logic.resources.
 Require Import algebra.cofe_solver.
 
 (* The Iris program logic is parametrized by a functor from the category of