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