yiyunliu/pair-eta
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

.

Browse source
This commit is contained in:
Yiyun Liu 2025-01-09 15:16:05 -05:00
parent 7021497615
commit 0d3b751a33
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
theories/logrel.v
View file

@ -603,8 +603,8 @@ Lemma ρ_ok_bot n (Γ : fin n -> Tm n) :
ρ_ok Γ (fun _ => Bot). ρ_ok Γ (fun _ => Bot).
Proof. Proof.
rewrite /ρ_ok. rewrite /ρ_ok.
move => i k PA. hauto q:on use:adequacy.
inversion i; subst. Qed. Qed.
Lemma ρ_ok_cons n i (Γ : fin n -> Tm n) ρ a PA A : Lemma ρ_ok_cons n i (Γ : fin n -> Tm n) ρ a PA A :
⟦ subst_Tm ρ A ⟧ i ↘ PA -> PA a -> ⟦ subst_Tm ρ A ⟧ i ↘ PA -> PA a ->