Elaboration of subtyping rule of struct and variant in SpecTec IL

[jihongmin63]

I elaborate the subtyping rule of struct and variant.

The current implementation did not strictly account for the premise-dropping behavior defined in the documentation. Specifically:

Variant types are in a subtype relation if the smaller type has fewer or the same number of cases, and for each of its cases there is an equivalent case in the larger type, except that the case in the larger type may drop some premises.

Record types are in a subtype relation if the larger type has fewer or the same number of fields, and for each of its fields there is an equivalent case in the smaller type, except that the field in the larger type may drop some premises.

So I categorized the premises for the smaller and the larger types, and revised the subtyping logic to ensure the larger type's premises are correctly contained within the smaller type's premises.
As there is no specific mention of this in the IL syntax, I would appreciate it if you could verify if this approach is correct.