TermSplicing1.agda:6,13-16
Set₁ !=< Term of type Set₂
when checking that the expression Set has type Term