diff --git a/theories/perm.v b/theories/perm.v
index 52f9eb2e343be0d85746bf078012996caee17f88..ff98376657d96071113652d77c54761442422360 100644
--- a/theories/perm.v
+++ b/theories/perm.v
@@ -91,6 +91,8 @@ Section duplicable.
 
 End duplicable.
 
+Hint Extern 0 (Is_true _.(ty_dup)) => exact I.
+
 Section has_type.
 
   Context `{iris_typeG Σ}.
diff --git a/theories/type.v b/theories/type.v
index 0e93d48f68a093116fedbe28db8dc2c8adf4ad1b..ab5148463c1af56f9f018354c13203992667f446 100644
--- a/theories/type.v
+++ b/theories/type.v
@@ -340,7 +340,7 @@ Section types.
       iMod ("Hclose2" with "[H2 H↦2]") as "[$$]". by iExists _; iFrame. done.
   Qed.
 
-  Definition product (tyl : list type) := fold_right product2 unit tyl.
+  Definition product := fold_right product2 unit.
 
   Lemma split_sum_mt l tid q tyl :
     (l ↦∗{q}: λ vl,
@@ -475,6 +475,7 @@ Notation "&uniq{ κ } ty" := (uniq_borrow κ ty)
 Notation "&shr{ κ } ty" := (shared_borrow κ ty)
   (format "&shr{ κ } ty", at level 20, right associativity) : lrust_type_scope.
 
+Arguments product : simpl never.
 Notation Π := product.
 (* Σ is commonly used for the current functor. So it cannot be defined
    as Π for products. We stick to the following form. *)
diff --git a/theories/typing.v b/theories/typing.v
index f797361a95aa08b5a592289b2059dee17454f6ba..c78fec77faad380bea82b986fc81582b8f2a1177 100644
--- a/theories/typing.v
+++ b/theories/typing.v
@@ -209,7 +209,7 @@ Section typing.
       iInduction vl as [|v vl] "IH". done.
       iExists [v], vl. iSplit. done. by iSplit.
     - assert (ty_size (Π (replicate (ty_size ty) uninit)) = ty_size ty) as ->; last by auto.
-      clear. induction ty.(ty_size). done. simpl in *. congruence.
+      clear. induction ty.(ty_size). done. by apply (f_equal S).
   Qed.
 
   Lemma consumes_copy_uniq_borrow ty κ κ' q: