shift_term_Hyb + typing

[Ayertienna]

Let shift be defined as:
Fixpoint shift_term_Hyb (M: te_Hyb) :=
match M with
| hyp_Hyb v => M
| lam_Hyb t M => lam_Hyb t (shift_term_Hyb M)
| appl_Hyb M1 M2 => appl_Hyb (shift_term_Hyb M1) (shift_term_Hyb M2)
| box_Hyb M => box_Hyb (shift_term_Hyb M)
| unbox_fetch_Hyb w M => unbox_fetch_Hyb (shift_vwo w) (shift_term_Hyb M)
| get_here_Hyb w M => get_here_Hyb (shift_vwo w) (shift_term_Hyb M)
| letdia_get_Hyb w M N => letdia_get_Hyb (shift_vwo w) (shift_term_Hyb M)
(shift_term_Hyb N)
end.

We have
G_Hyb |= (w', Gamma_Hyb) |- N ::: []A
We want
G_Hyb & (w'0, nil) |= (w', Gamma_Hyb)
|- {{fwo w'0 // bwo 0}}(shift_term_Hyb N) ::: []A

In particular, when trying to prove lemma:

Lemma shift_term_Hyb_types_Hyb:
forall N w G Gamma A w0,
G |= (w, Gamma) |- N ::: A ->
G |= (w, Gamma) |- (shift_term_Hyb N) ^w^ (fwo w0) ::: A.
by induction on typing of N, we get stuck in box case (and letdia, I guess).

(It can get stuck somewhere on the question whether w0 is a known world, but that's OK - we can add that..)

In particular for box case we want to show
G & (w0, Gamma0) |= (w', nil)
|- {{fwo w' // bwo 0}}({{fwo w1 // bwo 1}}(shift_term_Hyb M)) ::: A

but we have
G & (w0, Gamma0) |= (w', nil)
|- {{fwo w' // bwo 0}}({{fwo w' // bwo 1}}(shift_term_Hyb M)) ::: A

(Where w' is fresh and so far there are no assumptions on w', but we can add some. It is considered fresh where we want to use this lemma.)

[Ayertienna]

Can't do:
take

G |- (w, Gamma ) |- letdia_get w M (unbox_fetch 0 (hyp 0)) : A
(when G |- (w, Gamma) |- M ::: <>[]A)
if we shift letdia_get term, we are left with N = unbf 1 (hyp 0). This is not true for just any term to act as this 1...

[Ayertienna]

Dropped