+-- Make the coercion associated with a newtype. If we have
+--
+-- newtype T a b = MkT (Int, a, b)
+--
+-- Then (mkNewTypeCoercion CoT T [a,b] (Int, a, b)) creates the coercion
+-- CoT, such kinding rule such that
+--
+-- CoT S U :: (Int, S, U) :=: T S U