diff --git a/theories/typing/product.v b/theories/typing/product.v
index 73701ab9d775c8a481e9b1c973f47d60179e8b65..1881e59825c8fb9b98a6a1c0aa1364fbdd3c7eca 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -176,20 +176,21 @@ Section typing.
     - simpl. iFrame.
   Qed.
 
-  Lemma eqtype_prod_flatten E L tyl1 tyl2 tyl3 :
+  Lemma prod_flatten E L tyl1 tyl2 tyl3 :
     eqtype E L (Π(tyl1 ++ Π tyl2 :: tyl3)) (Π(tyl1 ++ tyl2 ++ tyl3)).
   Proof.
     unfold product. induction tyl1; simpl; last by f_equiv.
     induction tyl2. by rewrite left_id. by rewrite /= -assoc; f_equiv.
   Qed.
 
-  Lemma eqtype_prod_nil_flatten E L tyl1 tyl2 :
+  Lemma prod_flatten_l E L tyl1 tyl2 :
     eqtype E L (Π(Π tyl1 :: tyl2)) (Π(tyl1 ++ tyl2)).
-  Proof. apply (eqtype_prod_flatten _ _ []). Qed.
-  Lemma eqtype_prod_flatten_nil E L tyl1 tyl2 :
+  Proof. apply (prod_flatten _ _ []). Qed.
+  Lemma prod_flatten_r E L tyl1 tyl2 :
     eqtype E L (Π(tyl1 ++ [Π tyl2])) (Π(tyl1 ++ tyl2)).
-  Proof. by rewrite (eqtype_prod_flatten E L tyl1 tyl2 []) app_nil_r. Qed.
-  Lemma eqtype_prod_app E L tyl1 tyl2 :
+  Proof. by rewrite (prod_flatten E L tyl1 tyl2 []) app_nil_r. Qed.
+  Lemma prod_app E L tyl1 tyl2 :
     eqtype E L (Π[Π tyl1; Π tyl2]) (Π(tyl1 ++ tyl2)).
-  Proof. by rewrite -eqtype_prod_flatten_nil -eqtype_prod_nil_flatten. Qed.
+  Proof. by rewrite -prod_flatten_r -prod_flatten_l. Qed.
+
 End typing.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index aba596321c3a0a7130bc1cd24e21faedcd1b78c8..ba923d032991f6ffc0d3499c13340361fc99cda2 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -15,7 +15,7 @@ Section shr_bor.
   Qed.
 
   Global Instance subtype_shr_bor_mono E L :
-    Proper (lctx_lft_incl E L --> subtype E L ==> subtype E L) shr_bor.
+    Proper (flip (lctx_lft_incl E L) ==> subtype E L ==> subtype E L) shr_bor.
   Proof.
     intros κ1 κ2 Hκ ty1 ty2 Hty. apply subtype_simple_type.
     iIntros (??) "#LFT #HE #HL H". iDestruct (Hκ with "HE HL") as "#Hκ".
@@ -25,7 +25,7 @@ Section shr_bor.
     by iApply "Hs1".
   Qed.
   Global Instance subtype_shr_bor_mono' E L :
-    Proper (lctx_lft_incl E L ==> subtype E L --> flip (subtype E L)) shr_bor.
+    Proper (lctx_lft_incl E L ==> flip (subtype E L) ==> flip (subtype E L)) shr_bor.
   Proof. intros ??????. by apply subtype_shr_bor_mono. Qed.
   Global Instance subtype_shr_bor_proper E L κ :
     Proper (eqtype E L ==> eqtype E L) (shr_bor κ).
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index 2d496c4df5927f452e17bd6f60a13b46ffd905e7..4d0909526522fa10679e2f50d361aec1218a6d0f 100644
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
@@ -17,10 +17,10 @@ Section uninit.
   Lemma uninit_sz n : ty_size (uninit n) = n.
   Proof. induction n. done. simpl. by f_equal. Qed.
 
-  Lemma eqtype_uninit_product E L ns :
+  Lemma uninit_product E L ns :
     eqtype E L (uninit (foldr plus 0%nat ns)) (Π(uninit <$> ns)).
   Proof.
     induction ns as [|n ns IH]. done. revert IH.
-    by rewrite /= /uninit replicate_plus eqtype_prod_nil_flatten -!eqtype_prod_app=>->.
+    by rewrite /= /uninit replicate_plus prod_flatten_l -!prod_app=>->.
   Qed.
-End uninit.
\ No newline at end of file
+End uninit.