-mkAppCoercion, mkFunCoercion, mkTransCoercion, mkInstCoercion :: Coercion -> Coercion -> Coercion
-mkSymCoercion, mkLeftCoercion, mkRightCoercion :: Coercion -> Coercion
-mkAppsCoercion, mkInstsCoercion :: Coercion -> [Coercion] -> Coercion
-mkForAllCoercion :: Var -> Coercion -> Coercion
+-- | Apply a 'Coercion' to another 'Coercion', which is presumably a
+-- 'Coercion' constructor of some kind
+mkAppCoercion :: Coercion -> Coercion -> Coercion
+mkAppCoercion co1 co2 = mkAppTy co1 co2
+
+-- | Applies multiple 'Coercion's to another 'Coercion', from left to right.
+-- See also 'mkAppCoercion'
+mkAppsCoercion :: Coercion -> [Coercion] -> Coercion
+mkAppsCoercion co1 tys = foldl mkAppTy co1 tys