+allIdCos :: [CoercionI] -> Bool
+allIdCos = all isIdentityCoercion
+
+zipCoArgs :: [CoercionI] -> [Type] -> [Coercion]
+zipCoArgs cois tys = zipWith fromCoI cois tys
+
+fromCoI :: CoercionI -> Type -> Type
+fromCoI IdCo ty = ty -- Identity coercion represented
+fromCoI (ACo co) ty = co -- by the type itself
+