From 0d3b751a33f11fd0167126bf30107638f1fa53fe Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Thu, 9 Jan 2025 15:16:05 -0500 Subject: [PATCH] . --- theories/logrel.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/logrel.v b/theories/logrel.v index f0f72cb..05fb75d 100644 --- a/theories/logrel.v +++ b/theories/logrel.v @@ -603,8 +603,8 @@ Lemma ρ_ok_bot n (Γ : fin n -> Tm n) : ρ_ok Γ (fun _ => Bot). Proof. rewrite /ρ_ok. - move => i k PA. -inversion i; subst. Qed. + hauto q:on use:adequacy. +Qed. Lemma ρ_ok_cons n i (Γ : fin n -> Tm n) ρ a PA A : ⟦ subst_Tm ρ A ⟧ i ↘ PA -> PA a ->