Deduplicate prelude theorems

Author: Negabinary

src/language/proof/ProofHacks.re

@@ -556,3 +556,16 @@ let goal_of_typ = (ty: Typ.t): Exp.t => {
   | _ => Exp.fresh(Invalid("Bad_Goal"))
   };
 };
+
+let strip_theorems = (exp: Exp.t): Exp.t => {
+  Exp.map_term(
+    ~f_exp=
+      (cont, exp) => {
+        switch (exp |> Exp.term_of) {
+        | Theorem(_, _, e2) => cont(e2)
+        | _ => cont(exp)
+        }
+      },
+    exp,
+  );
+};

src/web/view/TheoremExerciseMode.re

@@ -225,10 +225,13 @@ module Update = {
     let stitched_scratch =
       Exercise.append_exp(just_prelude_term, just_lemmas_term);
     let stitched_theorem =
-      Exercise.append_exp(
-        stitched_scratch,
-        Language.Exp.replace_all_ids(just_prelude_term),
-      )
+      stitched_scratch
+      |> Exercise.append_exp(
+           _,
+           just_prelude_term
+           |> Language.ProofHacks.strip_theorems
+           |> Language.Exp.replace_all_ids,
+         )
       |> Exercise.append_exp(_, just_theorem_term);
 
     // Worker Setup