diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index aa7e252f5c2a2397eee0644201db7586fa55107e..a4e9cf07933d516c239bd298ab8afe48b54e6628 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -40,6 +40,9 @@ Class LanguageCtx (Λ : language) (K : expr Λ → expr Λ) := {
     ∃ e2', e2 = K e2' ∧ prim_step e1' σ1 e2' σ2 efs
 }.
 
+Instance language_ctx_id Λ : LanguageCtx Λ id.
+Proof. constructor; naive_solver. Qed.
+
 Section language.
   Context {Λ : language}.
   Implicit Types v : val Λ.