Add Hint Extern for Is_true/ty_dup. Make product simpl never (but that does...

Add Hint Extern for Is_true/ty_dup. Make product simpl never (but that does not work in many cases).

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 Σ}.

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. *)

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: