diff --git a/tests/lua/res1.lua b/tests/lua/res1.lua
new file mode 100644
index 0000000000..43d88d700d
--- /dev/null
+++ b/tests/lua/res1.lua
@@ -0,0 +1,120 @@
+-- Create names for commonly used constants
+local Or    = Const("or")
+local Not   = Const("not")
+local False = Const("false")
+
+function init_env(env)
+   -- Populate environment when declarations used by resolve_macro.
+   -- This is a 'fake' environment used only for testing.
+   local a   = Const("a")
+   local b   = Const("b")
+   local c   = Const("c")
+   local H   = Const("H")
+   env = add_decl(env, mk_var_decl("or",  mk_arrow(Bool, Bool, Bool)))
+   env = add_decl(env, mk_var_decl("not", mk_arrow(Bool, Bool)))
+   env = add_decl(env, mk_var_decl("false", Bool))
+   env = add_decl(env, mk_axiom("or_elim", Pi({{a, Bool}, {b, Bool}, {c, Bool}}, mk_arrow(Or(a, b), mk_arrow(a, c), mk_arrow(b, c), c))))
+   env = add_decl(env, mk_axiom("or_intro_left", Pi({{a, Bool}, {H, a}, {b, Bool}}, Or(a, b))))
+   env = add_decl(env, mk_axiom("or_intro_right", Pi({{b, Bool}, {a, Bool}, {H, b}}, Or(a, b))))
+   env = add_decl(env, mk_axiom("absurd_elim", Pi({{a, Bool}, {b, Bool}}, mk_arrow(a, Not(a), b))))
+   return env
+end
+
+function decl_bools(env, ls)
+   for i = 1, #ls do
+      env = add_decl(env, mk_var_decl(ls[i]:data(), Bool))
+   end
+   return env
+end
+
+function Consts(s)
+   -- Auxiliary function for creating multiple constants
+   local r = {}
+   local i = 1
+   for c in string.gmatch(s, '[^ ,;\t\n]+') do
+      r[i] = Const(c)
+      i = i + 1
+   end
+   return unpack(r)
+end
+
+function OR(...)
+   -- Nary Or
+   local arg = table.pack(...)
+   if     #arg == 0 then
+      return False
+   elseif #arg == 1 then
+      return arg[1]
+   else
+      local r = arg[#arg]
+      for i = #arg-1, 1, -1 do
+         r = Or(arg[i], r)
+      end
+      return r
+   end
+end
+
+function print_types(env, ...)
+   local arg = table.pack(...)
+   local tc  = type_checker(env)
+   for i = 1, #arg do
+      print(tostring(arg[i]) .. " : " .. tostring(tc:check(arg[i])))
+   end
+end
+
+function assert_some_axioms(env)
+   -- Assert some clauses
+   local l1, l2, l3, l4, l5, l6 = Consts("l1 l2 l3 l4 l5 l6")
+   env = decl_bools(env, {l1, l2, l3, l4, l5})
+   env = add_decl(env, mk_definition("l6", Bool, l3, {opaque=false})) -- l6 is alias for l3
+   env = add_decl(env, mk_axiom("H1", OR(l1, l2, Not(l3))))
+   env = add_decl(env, mk_axiom("H2", OR(l2, l3, l4)))
+   env = add_decl(env, mk_axiom("H3", OR(Not(l1), l2, l4, l5)))
+   env = add_decl(env, mk_axiom("H4", OR(l4, l6, Not(l5))))
+   env = add_decl(env, mk_axiom("H5", OR(Not(l4), l3)))
+   env = add_decl(env, mk_axiom("H6", Not(l3)))
+   env = add_decl(env, mk_axiom("H7", Not(l2)))
+   return env
+end
+
+local env = empty_environment({trust_lvl=1})
+env = init_env(env)
+env = assert_some_axioms(env)
+
+local l1, l2, l3, l4, l5, l6 = Consts("l1 l2 l3 l4 l5 l6")
+local H1, H2, H3, H4, H5, H6, H7 = Consts("H1 H2 H3 H4 H5 H6 H7")
+
+local tc  = type_checker(env)
+print(tc:check(Or))
+print(tc:check(Const("absurd_elim")))
+print(tc:check(H4))
+local Pr1 = resolve_macro(l6, H2, H1)
+local Pr2 = resolve_macro(l1, Pr1, H3)
+assert(Pr1:is_macro())
+assert(Pr1:macro_num_args() == 3)
+assert(Pr1:macro_arg(0) == l6)
+assert(Pr1:macro_def() == Pr2:macro_def())
+print("-----------")
+print(tc:check(H2))
+print(tc:check(H1))
+print(tc:check(Pr1))
+print(tc:check(H3))
+print(tc:check(Pr2))
+local Pr3 = resolve_macro(l4, resolve_macro(l5, Pr2, H4), H5)
+print(tc:check(Pr3))
+local Pr4 = resolve_macro(l2, resolve_macro(l3, Pr3, H6), H7)
+print("-----------")
+print("proof for false: ")
+print_types(env, H1, H2, H3, H4, H5, H6, H7)
+print(tostring(Pr4) .. " : " .. tostring(tc:check(Pr4)))
+
+print("----------------")
+print("Type checking again, but using trust_lvl=0, macros will be expanded during type checking")
+local env = empty_environment({trust_lvl=0})
+env = init_env(env)
+env = assert_some_axioms(env)
+local tc  = type_checker(env)
+-- Since the trust_lvl is 0, the macro will be expanded during type checking
+print(tc:whnf(Pr1))
+print(tc:check(Pr1))
+print(tc:check(Pr4))