local f = Const("f")
local a = Const("a")
local b = Const("b")
local x = Var(0)
assert(f(a, a):is_lt(f(a, b)))
assert(Const("a"):is_lt(Const("b")))
assert(Var(0):is_lt(Const("b")))
assert(name("a") < name("b"))
assert(not (Prop:is_lt(Prop)))
assert(not (Prop < Prop))
assert(mk_metavar("a", Prop):is_lt(mk_metavar("b", Prop)))
assert(not mk_metavar("a", Prop):is_lt(mk_metavar("a", Prop)))
assert(mk_metavar("a", Prop):is_lt(mk_metavar("a", Type)))
assert(mk_local("a", Prop):is_lt(mk_local("b", Prop)))
assert(not mk_local("a", Prop):is_lt(mk_local("a", Prop)))
assert(Prop:is_lt(Const("a")))
local a = Local("a", Prop)
local a1 = Local("a1", Type)
assert(Fun(a, a):is_lt(Fun(a1, a1)))
assert(Fun(a, a):is_lt(Fun(a, Var(2))))
assert(Pi(a, a):is_lt(Pi(a1, a1)))
assert(Pi(a, a):is_lt(Pi(a, Var(2))))
assert(Var(0) < Var(1))
print(Const("a", {mk_level_one(), mk_level_zero()}))
assert(Const("a", {mk_level_one()}):is_lt(Const("a", {mk_level_one(), mk_level_zero()})))
assert(Const("a", {mk_level_zero(), mk_level_one()}):is_lt(Const("a", {mk_level_one()})))
assert(not Const("a", {mk_level_zero(), mk_level_one()}):is_lt(Const("a", {mk_level_zero(), mk_level_one()})))