Function is_subtype 

pub fn is_subtype(ctx: &Context, a: &Term, b: &Term) -> bool

Check if type a is a subtype of type b (cumulativity).

Implements the subtyping relation for the Calculus of Constructions with cumulative universes.

Subtyping Rules

• Universe cumulativity: Type i <= Type j if i <= j
• Pi contravariance: Π(x:A). B <= Π(x:A'). B' if A' <= A and B <= B'
• Structural equality: Other terms are compared after normalization

Normalization

Both types are normalized before comparison, ensuring that definitionally equal types are recognized as subtypes.

Cumulativity Examples

• Type 0 <= Type 1 (lower universe is subtype of higher)
• Nat -> Type 0 <= Nat -> Type 1 (covariant in return type)
• Type 1 -> Nat <= Type 0 -> Nat (contravariant in parameter type)