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

Need to extend the notion of semwt to cover arbitrarily scoped terms

Browse source
This commit is contained in:
Yiyun Liu 2025-02-06 13:53:01 -05:00
parent fecac84977
commit 286ceeed39
1 changed files with 16 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
theories/logrel.v
View file

@ -800,10 +800,22 @@ Lemma SE_Bind n Γ i j p (A0 A1 : PTm n) B0 B1 :
Proof.
move => hA hB.
apply SemEq_SemWt in hA, hB.
apply SemWt_SemEq.
apply SemWt_SemEq; last by hauto l:on use:DJoin.BindCong.
hauto l:on use:ST_Bind.
apply ST_Bind; last by hauto l:on use:DJoin.BindCong. tauto.
(* rewrite SemWt_Univ. *)
(* move => ρ hρ /=. *)
apply ST_Bind; first by tauto.
move => ρ hρ.
suff : ρ_ok (funcomp (ren_PTm shift) (scons A0 Γ)) ρ by hauto l:on.
hauto l:on use:DJoin.BindCong.
rewrite /ρ_ok in hρ *.
move => j0 k PA.
destruct j0 as [j0|].
asimpl.
move /(_ (Some j0) k PA) : hρ. by asimpl.
asimpl.
move /(_ None k PA) : (hρ). asimpl.
have /SemWt_Univ h : Γ ⊨ A1 ∈ PUniv i by tauto.
have /h := hρ.
suff : DJoin.R (subst_PTm (funcomp ρ shift) A1) (subst_PTm (funcomp ρ shift) A0) by best use:InterpUniv_Join.