diff --git a/_CoqProject b/_CoqProject
index 7fa23825de9746b24ce7bb3dd460a0d68f3cf798..0cbaa47d1b3be5abaffccb25e7678c59568ee95c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -64,6 +64,7 @@ program_logic/viewshifts.v
 program_logic/wsat.v
 program_logic/ownership.v
 program_logic/weakestpre.v
+program_logic/weakestpre_fix.v
 program_logic/pviewshifts.v
 program_logic/resources.v
 program_logic/hoare.v
diff --git a/algebra/cofe.v b/algebra/cofe.v
index a6ef44bd472db862c97556a7a16583aac8167a6f..14941ef145361311a8c073813fe251ff0ec0a636 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -252,9 +252,11 @@ Infix "-n>" := cofe_mor (at level 45, right associativity).
 Instance cofe_more_inhabited {A B : cofeT} `{Inhabited B} :
   Inhabited (A -n> B) := populate (CofeMor (λ _, inhabitant)).
 
-(** Identity and composition *)
+(** Identity and composition and constant function *)
 Definition cid {A} : A -n> A := CofeMor id.
 Instance: Params (@cid) 1.
+Definition cconst {A B : cofeT} (x : B) : A -n> B := CofeMor (const x).
+Instance: Params (@cconst) 2.
 
 Definition ccompose {A B C}
   (f : B -n> C) (g : A -n> B) : A -n> C := CofeMor (f ∘ g).
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index edade4d96539fab7be61931e5a5ce3295c4435fb..b14d266236c4c9e6f80115f75a45fb1ce34768e4 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -15,7 +15,7 @@ Implicit Types σ : state Λ.
 Implicit Types P Q : iProp Λ Σ.
 Implicit Types Φ : val Λ → iProp Λ Σ.
 
-Notation wp_fork ef := (default True ef (flip (wp ⊤) (λ _, ■ True)))%I.
+Notation wp_fork ef := (default True ef (flip (wp ⊤) (λ _, True)))%I.
 
 Lemma wp_lift_step E1 E2
     (φ : expr Λ → state Λ → option (expr Λ) → Prop) Φ e1 σ1 :