diff --git a/_CoqProject b/_CoqProject
index 4de595c58b5312cf83897421606bde48ebf14d3b..c62d8f89395cc95956a3803a2bbec0e9d04254b8 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -44,7 +44,7 @@ theories/typing/cont.v
 theories/typing/fixpoint.v
 theories/typing/type_sum.v
 theories/typing/typing.v
-theories/typing/soundness.v
+theories/typing/adequacy.v
 theories/typing/tests/get_x.v
 theories/typing/tests/rebor.v
 theories/typing/tests/unbox.v
diff --git a/theories/typing/soundness.v b/theories/typing/adequacy.v
similarity index 90%
rename from theories/typing/soundness.v
rename to theories/typing/adequacy.v
index 6f2f7f0494c2ae0b5ebff45678213f8cb1dda609..674fdaa29aac4aba04868b2e9839eda863d1f19e 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/adequacy.v
@@ -18,13 +18,7 @@ Class typePreG Σ := PreTypeG {
 Definition typeΣ : gFunctors :=
   #[heapΣ; lftΣ; na_invΣ; GFunctor (constRF fracR)].
 Instance subG_typePreG {Σ} : subG typeΣ Σ → typePreG Σ.
-Proof.
-  split.
-  - apply subG_heapPreG. solve_inG.
-  - apply subG_lftPreG. solve_inG.
-  - solve_inG.
-  - solve_inG.
-Qed.
+Proof. solve_inG. Qed.
 
 Section type_soundness.
   Definition exit_cont : val := λ: [<>], #().
@@ -50,17 +44,15 @@ Section type_soundness.
     { by rewrite /elctx_interp big_sepL_nil. }
     { by rewrite /llctx_interp big_sepL_nil. }
     { by rewrite tctx_interp_nil. }
-    clear Hrtc Hmain main. iIntros (main) "(Htl & _ & _ & Hmain)".
+    clear Hrtc Hmain main. iIntros (main) "(Htl & HE & HL & Hmain)".
     rewrite tctx_interp_singleton. iDestruct "Hmain" as (?) "[EQ Hmain]".
     rewrite eval_path_of_val. iDestruct "EQ" as %[= <-].
     iDestruct "Hmain" as (f k x e ?) "(EQ & % & Hmain)". iDestruct "EQ" as %[= ->].
     destruct x; try done.
     iApply (wp_rec _ _ _ _ _ _ [exit_cont]%E); [done| |by simpl_subst|iNext].
     { repeat econstructor. apply to_of_val. }
-    iApply ("Hmain" $! () exit_cont [#] tid 1%Qp with "HEAP LFT Htl [] [] []");
+    iApply ("Hmain" $! () exit_cont [#] tid 1%Qp with "HEAP LFT Htl HE HL []");
       last by rewrite tctx_interp_nil.
-    { by rewrite /elctx_interp big_sepL_nil. }
-    { by rewrite /llctx_interp big_sepL_nil. }
     iIntros "_". rewrite cctx_interp_singleton. simpl. iIntros (args) "_ _".
     inv_vec args. iIntros (x) "_". by wp_seq.
   Qed.