diff --git a/theories/lang/races.v b/theories/lang/races.v
index 439161514d8d5d0f2a5031c2b743ab74d2b6db2a..5d78a388f498bf8ca840e04d2480b507d99dce43 100644
--- a/theories/lang/races.v
+++ b/theories/lang/races.v
@@ -201,7 +201,7 @@ Proof.
 
   destruct Ha1 as [[]|[]| | |], Ha2 as [[]|[]| | |]=>//=; simpl in *;
     repeat match goal with
-    | H : _ = Na1Ord → _ |- _ => specialize (H (reflexivity Na1Ord)) || clear H
+    | H : _ = Na1Ord → _ |- _ => specialize (H (eq_refl Na1Ord)) || clear H
     | H : False |- _ => destruct H
     | H : ∃ _, _ |- _ => destruct H
     end;
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index b77f8b33887229bda5e7df753feca8702c9fca41..0ae322ab26367de69ec9e9fd703cb7ab126d01ce 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -84,7 +84,7 @@ Section frac_bor.
     { change (qΦ + qq ≤ 1)%Qc in Hval. apply Qp_eq in HqΦq'. simpl in Hval, HqΦq'.
       rewrite <-HqΦq', <-Qcplus_le_mono_l in Hval. apply Qcle_lt_or_eq in Hval.
       destruct Hval as [Hval|Hval].
-      by left; apply ->Qclt_minus_iff. by right; apply Qp_eq, Qc_is_canon. }
+      by left; apply ->Qclt_minus_iff. right; apply Qp_eq, Qc_is_canon. by rewrite Hval. }
     - assert (q' = mk_Qp _ Hq'q + qq)%Qp as ->. { apply Qp_eq. simpl. ring. }
       iDestruct "Hq'κ" as "[Hq'qκ Hqκ]".
       iMod ("Hclose'" with "[HqΦ HΦqΦ Hown Hq'qκ]") as "Hqκ2".
diff --git a/theories/typing/perm_incl.v b/theories/typing/perm_incl.v
index 4e58a2614b345e35dab3fe5d39f9e267138e70ce..a29d8cb0d9e6bdd01ef2354f55fcef7c21ad3cc7 100644
--- a/theories/typing/perm_incl.v
+++ b/theories/typing/perm_incl.v
@@ -177,19 +177,18 @@ Section props.
         apply Qcplus_nonneg_nonneg. apply Qclt_le_weak, Qp_prf. done. }
       assert (q = q0 + mk_Qp _ Hpos)%Qp as ->. by by apply Qp_eq; rewrite -Hq.
       injection Hlen; intro Hlen'. rewrite perm_split_own_prod2 IH //.
-      apply perm_sep_proper.
+      set (q1l := q1::ql). cbn[combine_offs combine foldr]. apply perm_sep_proper.
       + rewrite /has_type /sep /=.
         destruct (eval_expr ν) as [[[]|]|]; split; iIntros (tid) "_ H/=";
         (try by iDestruct "H" as "[]"); (try by iDestruct "H" as (l) "[% _]");
         (try by auto); by rewrite shift_loc_0.
       + cut (length tyl = length (q1 :: ql)); last done. clear. revert tyl.
-        generalize 0%nat. induction (q1 :: ql)=>offs -[|ty tyl] Hlen //.
+        generalize 0%nat. induction (q1 :: ql)=>offs -[|ty tyl] Hlen //=.
         apply perm_sep_proper.
         * rewrite /has_type /sep /=.
           destruct (eval_expr ν) as [[[]|]|]; split; iIntros (tid) "_ H/=";
-          (try by iDestruct "H" as "[]"); (try by iDestruct "H" as (l) "[% _]");
-          (try by auto); by rewrite shift_loc_assoc_nat (comm plus).
-        * etransitivity. apply IHl. by injection Hlen. do 3 f_equiv. lia.
+          (try by iDestruct "H" as "[]"); [|]; by rewrite shift_loc_assoc_nat (comm plus).
+        * etrans. apply IHl. by injection Hlen. do 3 f_equiv. lia.
   Qed.
 
   Lemma perm_split_uniq_bor_prod2 ty1 ty2 κ ν :
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 506470f978cd0e492cc82631e6d8f0d74ad23a11..398506c67235bd54471d1f18db76468281d4885c 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -64,7 +64,7 @@ Record simple_type `{iris_typeG Σ} :=
     st_own_persistent tid vl : PersistentP (st_own tid vl) }.
 Global Existing Instance st_own_persistent.
 
-Program Coercion ty_of_st (st : simple_type) : type :=
+Program Definition ty_of_st (st : simple_type) : type :=
   {| ty_size := st.(st_size); ty_dup := true;
      ty_own := st.(st_own);
 
@@ -106,6 +106,8 @@ Qed.
 
 End type.
 
+Coercion ty_of_st : simple_type >-> type.
+
 Hint Extern 0 (Is_true _.(ty_dup)) =>
   exact I || assumption : typeclass_instances.