diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re
index 783d84e4f7..dcc743a968 100644
--- a/src/haz3lcore/dynamics/Elaborator.re
+++ b/src/haz3lcore/dynamics/Elaborator.re
@@ -199,6 +199,7 @@ let rec dhexp_of_uexp =
       | Test(test) =>
         let+ dtest = dhexp_of_uexp(m, test);
         DHExp.Test(id, dtest);
+      | Theorem(_) => Some(DHExp.Tuple([]))
       | Filter(act, cond, body) =>
         let* dcond = dhexp_of_uexp(~in_filter=true, m, cond);
         let+ dbody = dhexp_of_uexp(m, body);
diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re
index b43de49332..3c5d1cd176 100644
--- a/src/haz3lcore/lang/Form.re
+++ b/src/haz3lcore/lang/Form.re
@@ -103,6 +103,7 @@ let keywords = [
   "type",
   "case",
   "test",
+  "theorem",
   "if",
   "then",
   "else",
@@ -300,6 +301,7 @@ let forms: list((string, t)) = [
   ("ap_typ", mk(ii, ["(", ")"], mk_post(P.ap, Typ, [Typ]))),
   ("case", mk(ds, ["case", "end"], mk_op(Exp, [Rul]))),
   ("test", mk(ds, ["test", "end"], mk_op(Exp, [Exp]))),
+  ("theorem", mk(ds, ["theorem", "end"], mk_op(Exp, [Exp]))),
   ("fun_", mk(ds, ["fun", "->"], mk_pre(P.fun_, Exp, [Pat]))),
   (
     "rule",
@@ -328,6 +330,7 @@ let delims: list(Token.t) =
   |> List.fold_left((acc, (_, {label, _}: t)) => {label @ acc}, [])
   |> List.sort_uniq(compare);
 
+// TODO(nishant): do I need to handle theorem here too?
 let atomic_molds: Token.t => list(Mold.t) =
   s =>
     List.fold_left(
diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re
index 8fe8174dde..57d5596ca9 100644
--- a/src/haz3lcore/statics/MakeTerm.re
+++ b/src/haz3lcore/statics/MakeTerm.re
@@ -165,6 +165,7 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = {
         | term => ret(ListLit([term]))
         }
       | (["test", "end"], [Exp(test)]) => ret(Test(test))
+      | (["theorem", "end"], [Exp(theorem)]) => ret(Theorem(theorem))
       | (["case", "end"], [Rul({ids, term: Rules(scrut, rules)})]) => (
           Match(scrut, rules),
           ids,
diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
index 1d1beb302b..89bf516ef8 100644
--- a/src/haz3lcore/statics/Statics.re
+++ b/src/haz3lcore/statics/Statics.re
@@ -274,6 +274,10 @@ and uexp_to_info_map =
   | Test(e) =>
     let (e, m) = go(~mode=Ana(Bool), e, m);
     add(~self=Just(Prod([])), ~co_ctx=e.co_ctx, m);
+  // TODO(nishant): add code for Theorem here
+  | Theorem(e) =>
+    let (e, m) = go(~mode=Syn, e, m);
+    add(~self=Just(Prod([])), ~co_ctx=e.co_ctx, m);
   | Filter(_, cond, body) =>
     let (cond, m) = go(~mode, cond, m, ~is_in_filter=true);
     let (body, m) = go(~mode, body, m);
diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re
index a21a2cf596..d13f0deee8 100644
--- a/src/haz3lcore/statics/Term.re
+++ b/src/haz3lcore/statics/Term.re
@@ -447,7 +447,8 @@ module UExp = {
     | UnOp(op_un)
     | BinOp(op_bin)
     | Match
-    | ListConcat;
+    | ListConcat
+    | Theorem;
 
   let hole = (tms: list(any)): term =>
     switch (tms) {
@@ -488,7 +489,8 @@ module UExp = {
     | ListConcat(_) => ListConcat
     | UnOp(op, _) => UnOp(op)
     | BinOp(op, _, _) => BinOp(op)
-    | Match(_) => Match;
+    | Match(_) => Match
+    | Theorem(_) => Theorem;
 
   let show_op_un_meta: op_un_meta => string =
     fun
@@ -582,7 +584,8 @@ module UExp = {
     | ListConcat => "List Concatenation"
     | BinOp(op) => show_binop(op)
     | UnOp(op) => show_unop(op)
-    | Match => "Case expression";
+    | Match => "Case expression"
+    | Theorem => "Theorem";
 
   let rec is_fun = (e: t) => {
     switch (e.term) {
@@ -612,6 +615,7 @@ module UExp = {
     | UnOp(_)
     | BinOp(_)
     | Match(_)
+    | Theorem(_)
     | Constructor(_) => false
     };
   };
@@ -646,6 +650,7 @@ module UExp = {
       | UnOp(_)
       | BinOp(_)
       | Match(_)
+      | Theorem(_)
       | Constructor(_) => false
       }
     );
diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re
index e0f756b0dd..65fbaec9ed 100644
--- a/src/haz3lcore/statics/TermBase.re
+++ b/src/haz3lcore/statics/TermBase.re
@@ -122,6 +122,7 @@ and UExp: {
     | If
     | Seq
     | Test
+    | Theorem
     | Filter
     | Parens
     | Cons
@@ -152,6 +153,7 @@ and UExp: {
     | If(t, t, t)
     | Seq(t, t)
     | Test(t)
+    | Theorem(t)
     | Filter(FilterAction.t, t, t)
     | Parens(t) // (
     | Cons(t, t)
@@ -253,6 +255,7 @@ and UExp: {
     | If
     | Seq
     | Test
+    | Theorem
     | Filter
     | Parens
     | Cons
@@ -283,6 +286,7 @@ and UExp: {
     | If(t, t, t)
     | Seq(t, t)
     | Test(t)
+    | Theorem(t)
     | Filter(FilterAction.t, t, t)
     | Parens(t) // (
     | Cons(t, t)
diff --git a/src/haz3lcore/zipper/EditorUtil.re b/src/haz3lcore/zipper/EditorUtil.re
index e39b6bc59a..3fde12c9b6 100644
--- a/src/haz3lcore/zipper/EditorUtil.re
+++ b/src/haz3lcore/zipper/EditorUtil.re
@@ -60,6 +60,7 @@ let rec append_exp = (e1: TermBase.UExp.t, e2: TermBase.UExp.t) => {
   | Pipeline(_)
   | If(_)
   | Test(_)
+  | Theorem(_)
   | Parens(_)
   | Cons(_)
   | ListConcat(_)
diff --git a/src/haz3lschool/SyntaxTest.re b/src/haz3lschool/SyntaxTest.re
index b9a091403d..0d5230d559 100644
--- a/src/haz3lschool/SyntaxTest.re
+++ b/src/haz3lschool/SyntaxTest.re
@@ -51,6 +51,7 @@ let rec var_mention = (name: string, uexp: Term.UExp.t): bool => {
     find_var_upat(name, p)
       ? false : var_mention(name, def) || var_mention(name, body)
   | Test(u)
+  | Theorem(u)
   | Parens(u)
   | UnOp(_, u)
   | TyAlias(_, _, u)
@@ -97,6 +98,7 @@ let rec var_applied = (name: string, uexp: Term.UExp.t): bool => {
     find_var_upat(name, p)
       ? false : var_applied(name, def) || var_applied(name, body)
   | Test(u)
+  | Theorem(u)
   | Parens(u)
   | UnOp(_, u)
   | TyAlias(_, _, u)
@@ -189,6 +191,7 @@ let rec find_fn =
   | UnOp(_, u1)
   | TyAlias(_, _, u1)
   | Test(u1)
+  | Theorem(u1)
   | Filter(_, _, u1) => l |> find_fn(name, u1)
   | Ap(u1, u2)
   | Pipeline(u1, u2)
@@ -252,6 +255,7 @@ let rec tail_check = (name: string, uexp: Term.UExp.t): bool => {
     //If l has no recursive calls then true
     !List.fold_left((acc, ue) => {acc || var_mention(name, ue)}, false, l)
   | Test(_) => false
+  | Theorem(_) => false
   | TyAlias(_, _, u)
   | Filter(_, _, u)
   | Parens(u) => tail_check(name, u)
diff --git a/src/haz3lweb/view/ExplainThis.re b/src/haz3lweb/view/ExplainThis.re
index b8a4592847..4ce30cc957 100644
--- a/src/haz3lweb/view/ExplainThis.re
+++ b/src/haz3lweb/view/ExplainThis.re
@@ -1641,6 +1641,23 @@ let get_doc =
             ),
           TestExp.tests,
         );
+      // TODO(nishant): add explanation for Theorem(body) here in the style of Test above
+      | Theorem(body) =>
+        let body_id = List.nth(body.ids, 0);
+        get_message(
+          // TODO: add coloring for theorem
+          ~colorings=TestExp.test_exp_coloring_ids(~body_id),
+          ~format=
+            Some(
+              msg =>
+                Printf.sprintf(
+                  Scanf.format_from_string(msg, "%s"),
+                  Id.to_string(body_id),
+                ),
+            ),
+          // TODO change below to Theorem equivalent
+          TestExp.tests,
+        );
       | Parens(term) => get_message_exp(term.term) // No Special message?
       | Cons(hd, tl) =>
         let hd_id = List.nth(hd.ids, 0);