Dodgy newtype axioms

[Tim Chevalier]

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]
?

(Not asking for a proof or anything, just whether I'm drawing the
correct conclusion from your explanation.)

Thanks,
Tim

-- 
Tim Chevalier * http://cs.pdx.edu/~tjc * Often in error, never in doubt
"Well-behaved women rarely make history."  --Laurel Thatcher Ulrich