From c01717fbda5bf8e029cdbc96eba22f81c57dd696 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 21 Sep 2017 00:59:43 +0200
Subject: [PATCH] =?UTF-8?q?Prove=20`LanguageCtx=20=CE=9B=20id`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/program_logic/language.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index aa7e252f5..a4e9cf079 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 Λ.
-- 
GitLab