Prove subtyping case for soundness

[Ailrun]

C.f. #136

glu_univ_elem_per_subtyp_typ_if requires a way to relate OT' (satisfying {{ Γ, IT ⊢ OT' ® OP' d{{{ ⇑! a' (length Γ) }}} equiv_len'_len' }}) and OT'' (satisfying {{ Δ ⊢ OT'' ® OP' c equiv_c }})
but I am not sure if it is even possible.

[HuStmpHrrr]

Why do you need to come up with this type? I tend to believe you won't need the lemma you are trying to prove here.

[Ailrun]

Why do you need to come up with this type?

As I mentioned here: #136 (comment),
for subtyping cases, we need El to El', which then requires P to P' (as El depends on P).

[HuStmpHrrr]

right. I am saying glu_univ_elem_per_subtyp_typ_escape is all you need. you can just move on to proving the lemma about El. you probably won't need this lemma you are stuck at.

[Ailrun]

Now I think that might be the case. Let me check the actual subtyping case. If that's indeed the case, I will remove the stuck lemma and then the rest can be merged

[HuStmpHrrr]

yeah, I think the subtyping judgment is directly given by the semantic judgment in completeness, so you directly have the fact that the evaluations of two types are also in a subtyping relation. I think you can take it from there. You don't need a lemma that comes up with a type.

[HuStmpHrrr]

I think all you need is to add two premises to the subtyping rule, which says A and A' have type Type@i. Then you will have the right IHs which give you what you want. It will probably change some proofs of those syntactic lemmas, but to a livable extent.

[HuStmpHrrr]

sorry will review today. stay tuned.

[HuStmpHrrr]

I am sorry, this week was very bad for me. this PR looks almost ready to me.