diff --git a/gpfsl-examples/list_helper.v b/gpfsl-examples/list_helper.v
index 3c7ea936d1966f446d7f7441139a3d75e9205109..2f5e09ca515d01ec8f495856be1e544c5649c4be 100644
--- a/gpfsl-examples/list_helper.v
+++ b/gpfsl-examples/list_helper.v
@@ -45,7 +45,7 @@ Proof. apply prefix_app_inv. Qed.
 End prefixes.
 
 Global Instance fmap_prefix {A B} (f : A → B) :
-  Proper ((⊑) ==> (⊑)) (@fmap list _ _ _ f).
+  Proper ((⊑@{list _}) ==> (⊑)) (fmap f).
 Proof. intros L1 L2 [L3 Eq3]. rewrite Eq3. rewrite fmap_app. by eexists. Qed.
 
 Lemma lookup_fmap_Some' `{FinMap K M} {A B} (f : A → B) (m : M A) i y :
diff --git a/gpfsl/lang/lang.v b/gpfsl/lang/lang.v
index ec4dfeaceef6c8899099e4b6239fc3035e1b04cd..c7125e81a846c84116101d7ff6c16522e34d6c67 100644
--- a/gpfsl/lang/lang.v
+++ b/gpfsl/lang/lang.v
@@ -653,8 +653,8 @@ Module base.
        | _ => Lit LitPoison
        end) _).
     fix FIX 1. intros []; f_equal=>//; revert select (list expr); clear -FIX.
-    - fix FIX_INNER 1. intros []; [done|]. by simpl; f_equal.
-    - fix FIX_INNER 1. intros []; [done|]. by simpl; f_equal.
+    - fix FIX_INNER 1. intros []; [done|]. by f_equal/=.
+    - fix FIX_INNER 1. intros []; [done|]. by f_equal/=.
   Qed.
 
   Global Instance val_inhabited : Inhabited val := populate (LitV LitPoison).