Fix for contractive tweaks.

theories/logrel/session_types.v

@@ -114,9 +114,8 @@ Section session_types.
     intros Ss Ts Heq. rewrite /lty_choice.
     do 2 f_equiv. f_equiv => i.
     rewrite !lookup_total_alt.
-    specialize (Heq i).
-    destruct (Ss !! i), (Ts !! i);
-      [ f_contractive | contradiction | contradiction | done ].
+    specialize (Heq i). destruct (Ss !! i), (Ts !! i); simplify_eq/=; try done.
+    f_contractive.
     - f_equiv. split; intros H; eauto.
     - by rewrite Heq.
   Qed.

theories/logrel/term_types.v

@@ -115,7 +115,7 @@ Section term_types.
   Proof.
     intros A A' ? B B' ?. apply Ltty_ne=> v. f_equiv=> w.
     f_equiv; [by f_contractive|].
-    apply (wp_contractive _ _ _ _ _)=> v'. destruct n=> //=; by f_equiv.
+    apply (wp_contractive _ _ _ _ _)=> v'. f_contractive_core n' Hn'. by f_equiv.
   Qed.
   Global Instance lty_arr_ne `{heapGS Σ} : NonExpansive2 lty_arr.
   Proof. solve_proper. Qed.
@@ -135,7 +135,7 @@ Section term_types.
   Proof.
     intros F F' A. apply Ltty_ne=> w. f_equiv=> B.
     apply (wp_contractive _ _ _ _ _)=> u. specialize (A B).
-    by destruct n as [|n]; simpl.
+    f_contractive_core n' Hn'. by f_equiv.
   Qed.
   Global Instance lty_forall_ne `{heapGS Σ} k n :
     Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_forall Σ _ k).