diff --git a/semantics.opam b/semantics.opam
index 6f91b8e4711dea9bdc7bec944af14a3fe628d9c6..627e21ea85a387ba3abc6201b90aee61e92e97e6 100644
--- a/semantics.opam
+++ b/semantics.opam
@@ -9,9 +9,9 @@ bug-reports: "https://gitlab.mpi-sws.org/FP/semantics-course/issues"
 version: "dev"
 
 depends: [
-  "coq" { (>= "8.13" & < "8.17~") | (= "dev") }
-  "coq-iris-heap-lang" { (= "dev.2023-03-18.3.1b3e86bb") | (= "dev") }
-  "coq-equations" { (= "1.2.4+8.13") | (= "1.3+8.14") | (= "1.3+8.15")  | (= "1.3+8.16") }
+  "coq" { (>= "8.14" & < "8.18~") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2023-05-19.0.89b39c82") | (= "dev") }
+  "coq-equations" { (= "1.2.4+8.13") | (= "1.3+8.14") | (= "1.3+8.15")  | (= "1.3+8.16") | (= "1.3+8.17") }
   "coq-autosubst" { (= "1.7") | (= "dev")  }
 ]
 
diff --git a/theories/lib/debruijn.v b/theories/lib/debruijn.v
index 8561e52a088b2d2d39dd37acca77feb3c5314ffd..704a9bc4fd871efafa11172ad6c45dcda9d798eb 100644
--- a/theories/lib/debruijn.v
+++ b/theories/lib/debruijn.v
@@ -21,7 +21,7 @@ Lemma up_idss `{Ids X} `{Rename X} (sigma : var → X) n :
   up (idss n sigma) = idss (S n) (sigma >>> rename (+1) ).
 Proof.
   intros Hren_law.
-  f_ext. intros x. destruct x; unfold idss; simpl; first done.
+  f_ext. intros x. destruct x as [ | x]; unfold idss; simpl; first done.
   unfold up. simpl.
   destruct (decide (x < n)).
   - rewrite decide_True; last lia. apply Hren_law.
@@ -40,7 +40,7 @@ Qed.
 Lemma upren_idss sigma n :
   upren (idss n sigma) = idss (S n) (sigma >>> S).
 Proof.
-  f_ext. intros x. destruct x; unfold idss; simpl; first done.
+  f_ext. intros x. destruct x as [ | x]; unfold idss; simpl; first done.
   destruct (decide (x < n)).
   - rewrite decide_True; [done | lia ].
   - rewrite decide_False; lia.
diff --git a/theories/program_logics/concurrency.v b/theories/program_logics/concurrency.v
index 1c30fb7f3f7c7ce454d635d8adb85c6d063f5548..cd29c13d1edca07ae2177f2e930c5b7e0202b026 100644
--- a/theories/program_logics/concurrency.v
+++ b/theories/program_logics/concurrency.v
@@ -237,7 +237,8 @@ End with_lock.
 (** Exclusive Ghost Token *)
 Definition lockR : cmra := exclR unitO.
 Class lockG Σ :=
-  LockG { lockG_inG :> inG Σ lockR; }.
+  LockG { lockG_inG : inG Σ lockR; }.
+#[export] Existing Instance lockG_inG.
 Definition lockΣ : gFunctors := #[ GFunctor lockR ].
 Global Instance subG_lockΣ Σ : subG lockΣ Σ → lockG Σ.
 Proof. solve_inG. Qed.
diff --git a/theories/program_logics/concurrent_logrel/syntactic.v b/theories/program_logics/concurrent_logrel/syntactic.v
index 71da61e049d02a31ba13cbf42774bc7ddbb00fae..6e1edb3ab3a8bd1e3d62dba76bbdd230d255a9eb 100644
--- a/theories/program_logics/concurrent_logrel/syntactic.v
+++ b/theories/program_logics/concurrent_logrel/syntactic.v
@@ -258,24 +258,24 @@ Lemma type_wf_subst_dom σ τ n A:
   (∀ m, m < n → σ m = τ m) →
   A.[σ] = A.[τ].
 Proof.
-  induction 1 in σ, τ |-*; simpl; eauto.
+  induction 1 as [ | | | | ? A HA IH | ? A HA IH | ? A B HA IHA HB IHB | ? A B HA IHA HB IHB | ? A B HA IHA HB IHB | ? A HA IH | ? A HA IH] in σ, τ |-*; simpl; eauto.
   - (* tforall *)
     intros Heq; asimpl. f_equal.
-    eapply IHtype_wf; intros [|m]; rewrite /up; simpl; first done.
+    eapply IH; intros [|m]; rewrite /up; simpl; first done.
     intros Hlt. f_equal. eapply Heq. lia.
   - (* texists *)
     intros Heq; asimpl. f_equal.
-    eapply IHtype_wf. intros [ | m]; rewrite /up; simpl; first done.
+    eapply IH. intros [ | m]; rewrite /up; simpl; first done.
     intros Hlt. f_equal. apply Heq. lia.
   - (* fun *) intros ?. f_equal; eauto.
   - (* prod *) intros ?. f_equal; eauto.
   - (* sum *) intros ?. f_equal; eauto.
   - (* rec *)
     intros Heq; asimpl. f_equal.
-    eapply IHtype_wf; intros [|m]; rewrite /up; simpl; first done.
+    eapply IH; intros [|m]; rewrite /up; simpl; first done.
     intros Hlt. f_equal. eapply Heq. lia.
   - (* ref *)
-    intros ?. f_equal. eapply IHtype_wf. done.
+    intros ?. f_equal. eapply IH. done.
 Qed.
 
 Lemma type_wf_closed A σ:
diff --git a/theories/program_logics/heap_lang/adequacy.v b/theories/program_logics/heap_lang/adequacy.v
index 64b9ed1a4d0fef072947c334567af8720c86b73a..8592094e13ff9bb5cae5d80bc6cee092098a63fd 100644
--- a/theories/program_logics/heap_lang/adequacy.v
+++ b/theories/program_logics/heap_lang/adequacy.v
@@ -6,9 +6,11 @@ From semantics.pl.heap_lang Require Export proofmode.
 From iris.prelude Require Import options.
 
 Class heapGpreS Σ := HeapGpreS {
-  heapGpreS_iris :> invGpreS Σ;
-  heapGpreS_heap :> gen_heapGpreS loc (option val) Σ;
+  heapGpreS_iris : invGpreS Σ;
+  heapGpreS_heap : gen_heapGpreS loc (option val) Σ;
 }.
+#[export] Existing Instance heapGpreS_iris.
+#[export] Existing Instance heapGpreS_heap.
 
 Definition heapΣ : gFunctors :=
   #[invΣ; gen_heapΣ loc (option val)].
diff --git a/theories/program_logics/heap_lang/primitive_laws.v b/theories/program_logics/heap_lang/primitive_laws.v
index e749f58cea36a654dc23f2753b642d0f6c136c92..6ce0ff7c144a0f31cdfb31a10aa6ac2c4665829a 100644
--- a/theories/program_logics/heap_lang/primitive_laws.v
+++ b/theories/program_logics/heap_lang/primitive_laws.v
@@ -13,8 +13,9 @@ From iris.prelude Require Import options.
 
 Class heapGS Σ := HeapGS {
   heapGS_invGS : invGS_gen HasNoLc Σ;
-  heapGS_gen_heapGS :> gen_heapGS loc (option val) Σ;
+  heapGS_gen_heapGS : gen_heapGS loc (option val) Σ;
 }.
+#[export] Existing Instance heapGS_gen_heapGS.
 
 Global Instance heapGS_irisGS `{!heapGS Σ} : irisGS heap_lang Σ := {
   iris_invGS := heapGS_invGS;
diff --git a/theories/program_logics/heap_lang/proofmode.v b/theories/program_logics/heap_lang/proofmode.v
index 46da3d41187bdc55b95f45da026e1e112d1ec4a9..2f0ec79fcdca2e7ae30747feed4e4f9aebacbeb9 100644
--- a/theories/program_logics/heap_lang/proofmode.v
+++ b/theories/program_logics/heap_lang/proofmode.v
@@ -175,9 +175,9 @@ Implicit Types v : val.
 Implicit Types z : Z.
 
 Lemma wand_apply' (P R Q : iProp Σ) :
-  (P -∗ R) →
+  (P ⊢ R) →
   (R -∗ Q) →
-  P -∗ Q.
+  P ⊢ Q.
 Proof.
   intros Ha Hb. iIntros "HP". iApply Hb. iApply Ha. done.
 Qed.
@@ -229,7 +229,7 @@ Lemma tac_wp_free Δ Δ' s E1 E2 i K l v Φ :
   envs_entails Δ (WP fill K (Free (LitV l)) @ s; E1; E2 {{ Φ }}).
 Proof.
   rewrite envs_entails_unseal=> ? Hlk Hfin.
-  rewrite -wp_bind. eapply wand_apply; first exact: wp_free.
+  rewrite -wp_bind. eapply wand_apply; first apply wand_entails, wp_free.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   rewrite -Hfin wand_elim_r (envs_lookup_sound' _ _ _ _ _ Hlk).
   by apply later_mono, sep_mono_r.
@@ -242,7 +242,7 @@ Lemma tac_wp_load Δ Δ' s E1 E2 i K b l q v Φ :
   envs_entails Δ (WP fill K (Load (LitV l)) @ s; E1; E2 {{ Φ }}).
 Proof.
   rewrite envs_entails_unseal=> ?? Hi.
-  rewrite -wp_bind. eapply wand_apply; first exact: wp_load.
+  rewrite -wp_bind. eapply wand_apply; first apply wand_entails, wp_load.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   apply later_mono.
   destruct b; simpl.
@@ -261,7 +261,7 @@ Lemma tac_wp_store Δ Δ' s E1 E2 i K l v v' Φ :
 Proof.
   rewrite envs_entails_unseal=> ???.
   destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
-  rewrite -wp_bind. eapply wand_apply; first by eapply wp_store.
+  rewrite -wp_bind. eapply wand_apply; first apply wand_entails, wp_store.
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
diff --git a/theories/program_logics/logrel/ghost_state_lib.v b/theories/program_logics/logrel/ghost_state_lib.v
index d529e3438fe4bfaf3bb5ca765918fa7341bd90c0..3f8e6e358bb477a9a0654ab77beef609f493f390 100644
--- a/theories/program_logics/logrel/ghost_state_lib.v
+++ b/theories/program_logics/logrel/ghost_state_lib.v
@@ -89,7 +89,8 @@ End mononat.
 
 
 (** Half algebra: provides two halves *)
-Class halvesG Σ (A : Type) := HalvesG { halvesG_ghost_varG :> ghost_varG Σ A; }.
+Class halvesG Σ (A : Type) := HalvesG { halvesG_ghost_varG : ghost_varG Σ A; }.
+#[export] Existing Instance halvesG_ghost_varG.
 Definition halvesΣ A : gFunctors := ghost_varΣ A.
 Global Instance subG_halvesΣ Σ A : subG (halvesΣ A) Σ → halvesG Σ A.
 Proof. solve_inG. Qed.
@@ -132,7 +133,8 @@ Notation "'right'" := (ghalf) (only parsing).
 
 (** One shot *)
 Class oneshotG Σ (A : Type) :=
-  OneShotG { oneshotG_inG :> inG Σ (csumR (exclR unitO) (agreeR (leibnizO A))); }.
+  OneShotG { oneshotG_inG : inG Σ (csumR (exclR unitO) (agreeR (leibnizO A))); }.
+#[export] Existing Instance oneshotG_inG.
 Definition oneshotΣ A : gFunctors := #[ GFunctor (csumR (exclR unitO) (agreeR (leibnizO A))) ].
 Global Instance subG_oneshotΣ Σ A : subG (oneshotΣ A) Σ → oneshotG Σ A.
 Proof. solve_inG. Qed.
@@ -161,7 +163,7 @@ Section oneshot.
     os_pending γ -∗ |==> os_shot γ a.
   Proof.
     rewrite os_pending_eq os_shot_eq.
-    apply own_update.
+    iApply own_update.
     apply cmra_update_exclusive.
     done.
   Qed.
@@ -201,7 +203,8 @@ End oneshot.
 
 (** Agreement maps *)
 Class agmapG Σ (A B : Type) `{Countable A} :=
-  AgMapG { agmapG_inG :> ghost_mapG Σ A B; }.
+  AgMapG { agmapG_inG : ghost_mapG Σ A B; }.
+#[export] Existing Instance agmapG_inG.
 Definition agmapΣ A B `{Countable A} : gFunctors := ghost_mapΣ A B.
 Global Instance subG_agmapΣ Σ A B `{Countable A} : subG (agmapΣ A B) Σ → agmapG Σ A B.
 Proof. solve_inG. Qed.
diff --git a/theories/program_logics/program_logic/sequential_wp.v b/theories/program_logics/program_logic/sequential_wp.v
index 6b7fb5f35ec6a828e96e32dda1f84f0a4ff8a618..c4c0de57e388df67cbe78b4dd23f3639d88c2361 100644
--- a/theories/program_logics/program_logic/sequential_wp.v
+++ b/theories/program_logics/program_logic/sequential_wp.v
@@ -6,12 +6,13 @@ From iris.prelude Require Import options.
 Import uPred.
 
 Class irisGS (Λ : language) (Σ : gFunctors) := IrisG {
-  iris_invGS :> invGS_gen HasNoLc Σ;
+  iris_invGS : invGS_gen HasNoLc Σ;
 
   (** The state interpretation is an invariant that should hold in
   between each step of reduction. Here [state Λ] is the global state. *)
   state_interp : state Λ → iProp Σ;
 }.
+#[export] Existing Instance iris_invGS.
 Global Opaque iris_invGS.
 
 Definition wp_pre `{!irisGS Λ Σ} (s : stuckness)
diff --git a/theories/program_logics/reloc/ghost_state.v b/theories/program_logics/reloc/ghost_state.v
index de0da0c2db333a8f7b8a79b060c74184f70c96d5..968b42242c3163c10d4a0704e5318637623896f7 100644
--- a/theories/program_logics/reloc/ghost_state.v
+++ b/theories/program_logics/reloc/ghost_state.v
@@ -9,18 +9,24 @@ From iris Require Import prelude.
 
 
 Class reloc_preGS Σ := RelocPreGS {
-  reloc_preGS_heapG :> heapGpreS Σ;
-  reloc_preGS_sheapG :> ghost_mapG Σ loc (option val);
-  reloc_preGS_sexprG :> ghost_varG Σ expr;
+  reloc_preGS_heapG : heapGpreS Σ;
+  reloc_preGS_sheapG : ghost_mapG Σ loc (option val);
+  reloc_preGS_sexprG : ghost_varG Σ expr;
 }.
+#[export] Existing Instance reloc_preGS_heapG.
+#[export] Existing Instance reloc_preGS_sheapG.
+#[export] Existing Instance reloc_preGS_sexprG.
 
 Class relocGS Σ := RelocGS {
-  relocGS_heapG :> heapGS Σ;
-  relocGS_sheapG :> ghost_mapG Σ loc (option val);
-  relocGS_sexprG :> ghost_varG Σ expr;
+  relocGS_heapG : heapGS Σ;
+  relocGS_sheapG : ghost_mapG Σ loc (option val);
+  relocGS_sexprG : ghost_varG Σ expr;
   relocGS_sexpr_name : gname;
   relocGS_sheap_name : gname;
 }.
+#[export] Existing Instance relocGS_heapG.
+#[export] Existing Instance relocGS_sheapG.
+#[export] Existing Instance relocGS_sexprG.
 
 Definition relocΣ : gFunctors := #[heapΣ; ghost_mapΣ loc (option val); ghost_varΣ expr].
 Global Instance subG_relocΣ Σ : subG relocΣ Σ → reloc_preGS Σ.
diff --git a/theories/program_logics/reloc/proofmode.v b/theories/program_logics/reloc/proofmode.v
index f9e051d364b8d7f3c3661f7eca1540b88f80b0b2..e416ea58a9d8a438c6b9be9286f6af732b9e46ab 100644
--- a/theories/program_logics/reloc/proofmode.v
+++ b/theories/program_logics/reloc/proofmode.v
@@ -8,7 +8,17 @@ From semantics.pl.reloc Require Import ghost_state logrel.
 From iris.proofmode Require Import coq_tactics reduction spec_patterns.
 From iris.proofmode Require Export tactics.
 From semantics.pl.heap_lang Require Import primitive_laws.
+From iris.bi Require Import derived_laws.
+Import bi.
 From iris Require Import prelude.
+(*Import uPred.*)
+
+(*From iris.proofmode Require Import coq_tactics reduction spec_patterns.*)
+(*From iris.proofmode Require Export tactics.*)
+(*From iris.heap_lang Require Export tactics.*)
+(*From iris.heap_lang Require Import notation.*)
+(*From semantics.pl.heap_lang Require Export derived_laws.*)
+(*From semantics.pl.program_logic Require Export notation.*)
 
 
 Lemma tac_src_bind_gen `{relocGS Σ} Δ Δ' i p e e' Q :
@@ -69,7 +79,7 @@ Lemma src_expr_step_pure `{relocGS Σ} (ϕ : Prop) n e1 e2 K E :
   ϕ →
   PureExec ϕ n e1 e2 →
   ↑srcN ⊆ E →
-  src_expr (fill K e1) ={E}=∗ src_expr (fill K e2).
+  src_expr (fill K e1) ⊢ |={E}=> src_expr (fill K e2).
 Proof.
   iIntros (Hphi Hpure ?) "(#CTX & Hs)".
   iFrame "CTX". iApply src_step_pures; [ | done..]; done.
@@ -149,8 +159,8 @@ Tactic Notation "src_closure" := src_pure (Rec _ _ _).
 
 Lemma src_expr_step_store `{relocGS Σ} (v : val) (l : loc) v' K E :
   ↑srcN ⊆ E →
-  src_expr (fill K (#l <- v)) ∗ l ↦ₛ v' ={E}=∗
-  src_expr (fill K #()) ∗ l ↦ₛ v.
+  src_expr (fill K (#l <- v)) ∗ l ↦ₛ v' ⊢
+  |={E}=> src_expr (fill K #()) ∗ l ↦ₛ v.
 Proof.
   iIntros (?) "([#CTX Hs] & Hl)".
   iFrame "CTX". by iApply (src_step_store with "CTX Hs Hl").
@@ -203,8 +213,8 @@ Tactic Notation "src_store" :=
 
 Lemma src_expr_step_load `{relocGS Σ} (v : val) (l : loc) K E :
   ↑srcN ⊆ E →
-  src_expr (fill K (!#l)) ∗ l ↦ₛ v ={E}=∗
-  src_expr (fill K v) ∗ l ↦ₛ v.
+  src_expr (fill K (!#l)) ∗ l ↦ₛ v ⊢
+  |={E}=> src_expr (fill K v) ∗ l ↦ₛ v.
 Proof.
   iIntros (?) "([#CTX Hs] & Hl)".
   iFrame "CTX". by iApply (src_step_load with "CTX Hs Hl").
@@ -253,7 +263,8 @@ Tactic Notation "src_load" :=
 
 Lemma src_expr_step_alloc `{relocGS Σ} E K (v : val) :
   ↑srcN ⊆ E →
-  src_expr (fill K (ref v)) ={E}=∗ ∃ l : loc, src_expr (fill K (#l)) ∗ l ↦ₛ v.
+  src_expr (fill K (ref v)) ⊢
+  |={E}=> ∃ l : loc, src_expr (fill K (#l)) ∗ l ↦ₛ v.
 Proof.
   iIntros (?) "[#CTX Hs]".
   iFrame "CTX". by iApply (src_step_alloc with "CTX Hs").
diff --git a/theories/program_logics/resource_algebras.v b/theories/program_logics/resource_algebras.v
index 9e635b03f0958a2196eeeb71d587c9aa495cae72..381ea9a318207072c61218d39ff0d8b8b335a0ed 100644
--- a/theories/program_logics/resource_algebras.v
+++ b/theories/program_logics/resource_algebras.v
@@ -1613,7 +1613,8 @@ Canonical Structure prodCR (A B : lra) : cmra := cmra_of_lra (prod' A B) (prod_l
 
 (** We need this to register the ghost state we setup with Iris. *)
 Class mono_natG Σ :=
-  MonoNatG { mono_natG_inG :> inG Σ (authCR max_natUR); }.
+  MonoNatG { mono_natG_inG : inG Σ (authCR max_natUR); }.
+#[export] Existing Instance mono_natG_inG.
 Definition mono_natΣ : gFunctors := #[ GFunctor (authCR max_natUR) ].
 Global Instance subG_mono_natΣ Σ : subG mono_natΣ Σ → mono_natG Σ.
 Proof. solve_inG. Qed.
@@ -1668,7 +1669,8 @@ End mono_nat.
 
 (** ** Exercise: Oneshot *)
 Class oneshotG Σ (A : Type) `{Countable A} :=
-  OneShotG { oneshotG_inG :> inG Σ (csumCR (exclR unit) (agreeR A)); }.
+  OneShotG { oneshotG_inG : inG Σ (csumCR (exclR unit) (agreeR A)); }.
+#[export] Existing Instance oneshotG_inG.
 Definition oneshotΣ A `{Countable A} : gFunctors := #[ GFunctor (csumCR (exclR unit) (agreeR A)) ].
 Global Instance subG_oneshotΣ Σ A `{Countable A} : subG (oneshotΣ A) Σ → oneshotG Σ A.
 Proof. solve_inG. Qed.
@@ -1722,7 +1724,8 @@ End oneshot.
 
 (** ** Exercise: Synchronized Ghost State *)
 Class halvesG Σ (A : Type) :=
-  HalvesG { halvesG_inG :> inG Σ (authCR (optionUR (exclR A))); }.
+  HalvesG { halvesG_inG : inG Σ (authCR (optionUR (exclR A))); }.
+#[export] Existing Instance halvesG_inG.
 Definition halvesΣ A : gFunctors := #[ GFunctor (authCR (optionUR (exclR A))) ].
 Global Instance subG_halvesΣ Σ A : subG (halvesΣ A) Σ → halvesG Σ A.
 Proof. solve_inG. Qed.
@@ -1758,7 +1761,8 @@ Section halves.
 End halves.
 
 (** ** Exercise: gvar *)
-Class gvarG Σ (A : Type) `{Countable A} := GvarG { gvarG_inG :> inG Σ (prodCR fracR (agreeR A)); }.
+Class gvarG Σ (A : Type) `{Countable A} := GvarG { gvarG_inG : inG Σ (prodCR fracR (agreeR A)); }.
+#[export] Existing Instance gvarG_inG.
 Definition gvarΣ A `{Countable A} : gFunctors := #[ GFunctor (prodCR fracR (agreeR A)) ].
 Global Instance subG_gvarΣ Σ A `{Countable A} : subG (gvarΣ A) Σ → gvarG Σ A.
 Proof. solve_inG. Qed.
@@ -1817,7 +1821,8 @@ End gvar.
 (** Agreement maps *)
 Definition agmapCR (A B : Type) `{Countable A} `{Countable B} := (authCR (gmapUR A (agreeR B))).
 Class agmapG Σ (A B : Type) `{Countable A} `{Countable B} :=
-  AgMapG { agmapG_inG :> inG Σ (agmapCR A B); }.
+  AgMapG { agmapG_inG : inG Σ (agmapCR A B); }.
+#[export] Existing Instance agmapG_inG.
 Definition agmapΣ A B `{Countable A} `{Countable B} : gFunctors := #[ GFunctor (agmapCR A B) ].
 Global Instance subG_agmapΣ Σ A B `{Countable A} `{Countable B} : subG (agmapΣ A B) Σ → agmapG Σ A B.
 Proof. solve_inG. Qed.
@@ -1867,7 +1872,8 @@ End agmap.
 (** Updateable maps *)
 Definition exmapCR (A B : Type) `{Countable A} := (authCR (gmapUR A (exclR B))).
 Class exmapG Σ (A B : Type) `{Countable A} :=
-  ExMapG { exmapG_inG :> inG Σ (exmapCR A B); }.
+  ExMapG { exmapG_inG : inG Σ (exmapCR A B); }.
+#[export] Existing Instance exmapG_inG.
 Definition exmapΣ A B `{Countable A} : gFunctors := #[ GFunctor (exmapCR A B) ].
 Global Instance subG_exmapΣ Σ A B `{Countable A} : subG (exmapΣ A B) Σ → exmapG Σ A B.
 Proof. solve_inG. Qed.
diff --git a/theories/type_systems/stlc_extended/lang.v b/theories/type_systems/stlc_extended/lang.v
index b075ae92aecb8a9dd7dfc22d563ac2590465a217..5f439a7bb803693c1ac78ca9815a4558afae65ee 100644
--- a/theories/type_systems/stlc_extended/lang.v
+++ b/theories/type_systems/stlc_extended/lang.v
@@ -89,13 +89,14 @@ Fixpoint is_val (e : expr) : Prop :=
   end.
 Lemma is_val_spec e : is_val e ↔ ∃ v, to_val e = Some v.
 Proof.
-  induction e; simpl; (split; [ | intros (v & Heq)]); simplify_option_eq; try done; eauto.
-  - rewrite IHe1, IHe2. intros [(v1 & ->) (v2 & ->)]. eauto.
-  - rewrite IHe1, IHe2. eauto.
-  - rewrite IHe. intros (v & ->). eauto.
-  - apply IHe. eauto.
-  - rewrite IHe. intros (v & ->); eauto.
-  - apply IHe. eauto.
+  induction e as [ | | ? e IH | e1 IH1 e2 IH2 | ? e1 IH1 e2 IH2 | e1 IH1 e2 IH2 | e IH | e IH | e IH | e IH | e1 IH1 e2 IH2 e3 IH3];
+    simpl; (split; [ | intros (v & Heq)]); simplify_option_eq; try done; eauto.
+  - rewrite IH1, IH2. intros [(v1 & ->) (v2 & ->)]. eauto.
+  - rewrite IH1, IH2. eauto.
+  - rewrite IH. intros (v & ->). eauto.
+  - apply IH. eauto.
+  - rewrite IH. intros (v & ->); eauto.
+  - apply IH. eauto.
 Qed.
 
 Ltac simplify_val :=
diff --git a/theories/type_systems/systemf/lang.v b/theories/type_systems/systemf/lang.v
index fee6a9092b4bc61708c493a596c86f165988da13..e7992cff2d7447873253065871ed70b4884fc441 100644
--- a/theories/type_systems/systemf/lang.v
+++ b/theories/type_systems/systemf/lang.v
@@ -108,15 +108,16 @@ Fixpoint is_val (e : expr) : Prop :=
   end.
 Lemma is_val_spec e : is_val e ↔ ∃ v, to_val e = Some v.
 Proof.
-  induction e; simpl; (split; [ | intros (v & Heq)]); simplify_option_eq; try done; eauto.
-  - rewrite IHe. intros (v & ->); eauto.
-  - apply IHe. eauto.
-  - rewrite IHe1, IHe2. intros [(v1 & ->) (v2 & ->)]. eauto.
-  - rewrite IHe1, IHe2. eauto.
-  - rewrite IHe. intros (v & ->). eauto.
-  - apply IHe. eauto.
-  - rewrite IHe. intros (v & ->); eauto.
-  - apply IHe. eauto.
+  induction e as [ | | ? e IH | e1 IH1 e2 IH2 | e IH | ? e1 IH1 e2 IH2 | e1 IH1 e2 IH2 e3 IH3 | e IH | e IH | e IH | ? e1 IH1 e2 IH2 | e1 IH1 e2 IH2 | e IH | e IH | e IH | e IH | e1 IH1 e2 IH2 e3 IH3 ];
+    simpl; (split; [ | intros (v & Heq)]); simplify_option_eq; try done; eauto.
+  - rewrite IH. intros (v & ->). eauto.
+  - apply IH. eauto.
+  - rewrite IH1, IH2. intros [(v1 & ->) (v2 & ->)]. eauto.
+  - rewrite IH1, IH2. eauto.
+  - rewrite IH. intros (v & ->). eauto.
+  - apply IH. eauto.
+  - rewrite IH. intros (v & ->); eauto.
+  - apply IH. eauto.
 Qed.
 
 Ltac simplify_val :=
diff --git a/theories/type_systems/systemf_mu/lang.v b/theories/type_systems/systemf_mu/lang.v
index b07b84772e38dff017054b23d1fd3fe72ad31a0e..6261b43df2af9e8c0bc12ad4aec16ddd3eec43db 100644
--- a/theories/type_systems/systemf_mu/lang.v
+++ b/theories/type_systems/systemf_mu/lang.v
@@ -116,17 +116,13 @@ Fixpoint is_val (e : expr) : Prop :=
   end.
 Lemma is_val_spec e : is_val e ↔ ∃ v, to_val e = Some v.
 Proof.
-  induction e; simpl; (split; [ | intros (v & Heq)]); simplify_option_eq; try done; eauto.
-  - rewrite IHe. intros (v & ->); eauto.
-  - apply IHe. eauto.
-  - rewrite IHe1, IHe2. intros [(v1 & ->) (v2 & ->)]. eauto.
-  - rewrite IHe1, IHe2. eauto.
-  - rewrite IHe. intros (v & ->). eauto.
-  - apply IHe. eauto.
-  - rewrite IHe. intros (v & ->); eauto.
-  - apply IHe. eauto.
-  - rewrite IHe. intros (v & ->). eauto.
-  - apply IHe. eauto.
+  induction e as [ | | ? e IH | e1 IH1 e2 IH2 | e IH | ? e1 IH1 e2 IH2 | e1 IH1 e2 IH2 e3 IH3 | e IH | e IH | e IH | ? e1 IH1 e2 IH2 | e1 IH1 e2 IH2 | e IH | e IH | e IH | e IH | e1 IH1 e2 IH2 e3 IH3 | e IH | e IH];
+    simpl; (split; [ | intros (v & Heq)]); simplify_option_eq; try naive_solver.
+  - rewrite IH. intros (v & ->). eauto.
+  - rewrite IH1, IH2. intros [(v1 & ->) (v2 & ->)]. eauto.
+  - rewrite IH. intros (v & ->). eauto.
+  - rewrite IH. intros (v & ->); eauto.
+  - rewrite IH. intros (v & ->). eauto.
 Qed.
 
 Global Instance base_lit_eq_dec : EqDecision base_lit.
diff --git a/theories/type_systems/systemf_mu/untyped_encoding.v b/theories/type_systems/systemf_mu/untyped_encoding.v
index f85f267fd18ce848b7ea275d126f91da349fcac3..5c42452b195c0f2b88d3084e5d8f715c5fb64c5b 100644
--- a/theories/type_systems/systemf_mu/untyped_encoding.v
+++ b/theories/type_systems/systemf_mu/untyped_encoding.v
@@ -63,7 +63,7 @@ Lemma Ω_loops:
 Proof.
   econstructor 2; [|econstructor 1].
   - rewrite /Ω /ω. eauto.
-  - rewrite /Ω. eauto. eapply app_step_beta; eauto.
+  - rewrite /Ω. eauto.
 Qed.
 
 Lemma ω_typed :
diff --git a/theories/type_systems/systemf_mu_state/lang.v b/theories/type_systems/systemf_mu_state/lang.v
index 8f5c3b4a7609db56218d0b64a6cf9895ce5f3ac5..fc0a0550418e10347e5b05c64571d16a06327387 100644
--- a/theories/type_systems/systemf_mu_state/lang.v
+++ b/theories/type_systems/systemf_mu_state/lang.v
@@ -121,17 +121,13 @@ Fixpoint is_val (e : expr) : Prop :=
   end.
 Lemma is_val_spec e : is_val e ↔ ∃ v, to_val e = Some v.
 Proof.
-  induction e; simpl; (split; [ | intros (v & Heq)]); simplify_option_eq; try done; eauto.
-  - rewrite IHe. intros (v & ->); eauto.
-  - apply IHe. eauto.
-  - rewrite IHe1 IHe2. intros [(v1 & ->) (v2 & ->)]. eauto.
-  - rewrite IHe1 IHe2. eauto.
-  - rewrite IHe. intros (v & ->). eauto.
-  - apply IHe. eauto.
-  - rewrite IHe. intros (v & ->); eauto.
-  - apply IHe. eauto.
-  - rewrite IHe. intros (v & ->). eauto.
-  - apply IHe. eauto.
+  induction e as [ | | ? e IH | e1 IH1 e2 IH2 | e IH | ? e1 IH1 e2 IH2 | e1 IH1 e2 IH2 e3 IH3 | e IH | e IH | e IH | ? e1 IH1 e2 IH2 | e1 IH1 e2 IH2 | e IH | e IH | e IH | e IH | e1 IH1 e2 IH2 e3 IH3 | e IH | e IH | | | ];
+    simpl; (split; [ | intros (v & Heq)]); simplify_option_eq; try naive_solver.
+  - rewrite IH. intros (v & ->). eauto.
+  - rewrite IH1 IH2. intros [(v1 & ->) (v2 & ->)]. eauto.
+  - rewrite IH. intros (v & ->). eauto.
+  - rewrite IH. intros (v & ->); eauto.
+  - rewrite IH. intros (v & ->). eauto.
 Qed.
 
 Global Instance base_lit_eq_dec : EqDecision base_lit.