Why do we need this premise?

[HuStmpHrrr]

McTT/theories/Core/Syntactic/System/Definitions.v

Line 86 in c33ec07

(** We have this extra argument for soundness.

Why is this? @Ailrun Things like this are good to recall, as we might need to talk about them in the paper.

[Ailrun]

In soundness case for the rule, we have syntactic A sub A' judgement and semantic M : A judgement. We cannot obtain semantic well-formedness of A' from these, thus we should have it as an IH.

[HuStmpHrrr]

I think it has something to do with subtyping being unidirectional. see also

McTT/theories/Core/Soundness/SubtypingCases.v

Lines 91 to 94 in c01fbc9

	Lemma glu_rel_exp_conv : forall {Γ M A A' i},
	{{ Γ ⊩ M : A }} ->
	{{ Γ ⊢ A ≈ A' : Type@i }} ->
	{{ Γ ⊩ M : A' }}.

This lemma doesn't need the semantic well-formedness of A'.

[Ailrun]

Hm, that might the case for subtyping as well. I mean, completeness might resolve the need of the extra IH.

[Ailrun]

Or not. As you said, it is uni-directional so one cannot prove an analogous lemma of

McTT/theories/Core/Soundness/LogicalRelation/CoreLemmas.v

Lines 639 to 642 in c33ec07

	Lemma glu_univ_elem_resp_per_univ : forall i a a' P El,
	{{ Dom a ≈ a' ∈ per_univ i }} ->
	{{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
	{{ DG a' ∈ glu_univ_elem i ↘ P ↘ El }}.

for semantic subtyping.