From 05ec7cc95f73876012989b242f1a94392f0b7540 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de>
Date: Tue, 17 Dec 2024 17:47:49 +0100
Subject: [PATCH] fix
---
theories/type_systems/systemf/church_encodings_faithful.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/type_systems/systemf/church_encodings_faithful.v b/theories/type_systems/systemf/church_encodings_faithful.v
index d28a947..4620898 100644
--- a/theories/type_systems/systemf/church_encodings_faithful.v
+++ b/theories/type_systems/systemf/church_encodings_faithful.v
@@ -265,9 +265,9 @@ Proof.
+ simpl. bs_step_det.
rewrite subst_is_closed_nil; first by apply big_step_of_val.
apply sem_type_closed_val in Ha12. naive_solver.
- + simp type_interp.
+ + by simp type_interp.
- simp type_interp. exists b1, b2. split_and!.
+ by apply big_step_of_val.
+ simpl. bs_step_det. by apply big_step_of_val.
- + simp type_interp.
+ + by simp type_interp.
Qed.
--
GitLab