Issue478.agda:12,9-12
Set₁ !=< T of type Set₂
when checking that the expression Set has type T