diff --git a/theories/typing/adequacy.v b/theories/typing/adequacy.v
index 6f2f7f0494c2ae0b5ebff45678213f8cb1dda609..7b4eff80ee483898653d1b03ceab7fb97db72457 100644
--- a/theories/typing/adequacy.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 := λ: [<>], #().