diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re
index a3fb151d11..4027ee9d25 100644
--- a/src/haz3lcore/dynamics/Elaborator.re
+++ b/src/haz3lcore/dynamics/Elaborator.re
@@ -200,7 +200,7 @@ let rec dhexp_of_uexp =
       | Test(test) =>
         let+ dtest = dhexp_of_uexp(m, test);
         DHExp.Test(id, dtest);
-      | Theorem(_, _, _) => Some(DHExp.Tuple([]))
+      | Theorem(_, _, e) => dhexp_of_uexp(m, e)
       | Filter(act, cond, body) =>
         let* dcond = dhexp_of_uexp(~in_filter=true, m, cond);
         let+ dbody = dhexp_of_uexp(m, body);