diff --git a/theories/typing/product.v b/theories/typing/product.v
index 5efbb086415f8c267b0507c29bc9172fe74f5183..e415a89190e7d5e87844fde7032ba904bcf4607c 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -118,9 +118,17 @@ Section product.
   Qed.
 
   Definition product := foldr product2 unit.
-  (* Given that in practice, product will be used with concrete lists,
-     there should be no need to declare [Copy] and [Proper] instances
-     for [product]. *)
+
+  Global Instance product_mono E L:
+    Proper (Forall2 (subtype E L) ==> subtype E L) product.
+  Proof. intros ??. induction 1. done. by simpl; f_equiv. Qed.
+  Global Instance product_proper E L:
+    Proper (Forall2 (eqtype E L) ==> eqtype E L) product.
+  Proof. intros ??. induction 1. done. by simpl; f_equiv. Qed.
+  (* FIXME : this instance is never going to be used, because Forall is
+     not a typeclass. *)
+  Global Instance product_copy tys : Forall Copy tys → Copy (product tys).
+  Proof. induction 1; apply _. Qed.
 End product.
 
 Arguments product : simpl never.
@@ -174,4 +182,14 @@ Section typing.
     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 :
+    eqtype E L (Π(Π tyl1 :: tyl2)) (Π(tyl1 ++ tyl2)).
+  Proof. apply (eqtype_prod_flatten _ _ []). Qed.
+  Lemma eqtype_prod_flatten_nil 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 :
+    eqtype E L (Π[Π tyl1; Π tyl2]) (Π(tyl1 ++ tyl2)).
+  Proof. by rewrite -eqtype_prod_flatten_nil -eqtype_prod_nil_flatten. Qed.
 End typing.
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index 7fc9fa0e0e04a8f48a718b7e30de858253a62964..2d496c4df5927f452e17bd6f60a13b46ffd905e7 100644
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
@@ -11,14 +11,16 @@ Section uninit.
   Definition uninit (n : nat) : type :=
     Π (replicate n uninit_1).
 
+  Global Instance uninit_copy n : Copy (uninit n).
+  Proof. apply product_copy, Forall_replicate, _. Qed.
+
+  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 :
     eqtype E L (uninit (foldr plus 0%nat ns)) (Π(uninit <$> ns)).
   Proof.
-    induction ns as [|n ns IH]. done.
-    rewrite /= /uninit replicate_plus (eqtype_prod_flatten E L []).
-    induction n. done. rewrite /product /=. by f_equiv.
+    induction ns as [|n ns IH]. done. revert IH.
+    by rewrite /= /uninit replicate_plus eqtype_prod_nil_flatten -!eqtype_prod_app=>->.
   Qed.
-
-  Lemma uninit_sz n : ty_size (uninit n) = n.
-  Proof. induction n. done. simpl. by f_equal. Qed.
 End uninit.
\ No newline at end of file