| So would it be correct to claim that: | | if k1 <: k2 | and (T1::k1) and (t2::k2) for some type T1 and tyvar t2 | and A :=: B is an equality axiom | then A[T1/t2] :=: B[T1/t2] | ? Yes, I think that's right. For example if t2:?, then t2 ranges over arbitrary types, including unboxed ones. So you can substitute Int# : # for it. Or Int:*. Simon