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

Finish (simplified) SE_Bind

Browse source
This commit is contained in:
Yiyun Liu 2025-02-06 14:37:56 -05:00
parent 1258ac263c
commit 435c0e037e
1 changed files with 1 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

20
theories/logrel.v
View file

@ -851,23 +851,5 @@ Proof.
move => ρ hρ. move => ρ hρ.
suff : ρ_ok (funcomp (ren_PTm shift) (scons A0 Γ)) ρ by hauto l:on. suff : ρ_ok (funcomp (ren_PTm shift) (scons A0 Γ)) ρ by hauto l:on.
move : Γ_eq_ρ_ok hΓ' hρ; repeat move/[apply]. apply. move : Γ_eq_ρ_ok hΓ' hρ; repeat move/[apply]. apply.
hauto lq:on use:Γ_eq_cons'.
best use:
move => j0 k PA.
destruct j0 as [j0|].
asimpl.
move /(_ (Some j0) k PA) : hρ. by asimpl.
asimpl.
have h : Γ ⊨ A1 ∈ PUniv i by tauto.
rewrite /SemWff in hΓ'.
move /(_ None) : hΓ' => [l h'].
rewrite SemWt_Univ in h'.
have {}/h' := hρ.
move => [PA'].
asimpl. move => h0 h1.
move /(_ None l PA) : (hρ). asimpl.
suff : PA = PA' by qauto l:on.
move : InterpUniv_Join' h1 h0; repeat move/[apply].
apply. apply DJoin.substing. tauto.
Qed. Qed.