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