diff --git a/stage0/stdlib/Lean/Compiler/IR/EmitC.c b/stage0/stdlib/Lean/Compiler/IR/EmitC.c
index 9469cfd6fc03..9298eb4d6471 100644
--- a/stage0/stdlib/Lean/Compiler/IR/EmitC.c
+++ b/stage0/stdlib/Lean/Compiler/IR/EmitC.c
@@ -247,7 +247,6 @@ lean_object* l_Lean_IR_EmitC_emitUSet(lean_object*, lean_object*, lean_object*,
 static lean_object* l_String_foldlAux___at_Lean_IR_EmitC_quoteString___spec__1___closed__4;
 LEAN_EXPORT lean_object* l_Nat_forM_loop___at_Lean_IR_EmitC_emitArgs___spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_IR_EmitC_overwriteParam(lean_object*, lean_object*);
-static lean_object* l_Lean_IR_EmitC_shouldExport___closed__12;
 extern lean_object* l_Lean_exportAttr;
 LEAN_EXPORT lean_object* l_List_forM___at_Lean_IR_EmitC_emitLns___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_IR_EmitC_emitTailCall___closed__1;
@@ -422,7 +421,6 @@ static lean_object* l_Lean_IR_EmitC_emitMainFn___lambda__2___closed__30;
 static lean_object* l_Lean_IR_EmitC_emitInitFn___closed__7;
 extern lean_object* l_Lean_NameSet_empty;
 static lean_object* l_List_forM___at_Lean_IR_EmitC_emitFnDecls___spec__5___closed__1;
-static lean_object* l_Lean_IR_EmitC_shouldExport___closed__13;
 static lean_object* l_Lean_IR_EmitC_emitPartialApp___closed__2;
 static lean_object* l_Lean_IR_EmitC_emitDeclAux___lambda__3___closed__2;
 lean_object* l_Lean_IR_EmitC_emitCtorScalarSize(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -604,7 +602,6 @@ static lean_object* l_Lean_IR_EmitC_emitMainFn___lambda__2___closed__7;
 lean_object* l_Lean_IR_collectUsedDecls(lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_IR_EmitC_emitMainFn___lambda__1___closed__15;
 static lean_object* l_Lean_IR_EmitC_emitMainFn___lambda__2___closed__16;
-static lean_object* l_Lean_IR_EmitC_shouldExport___closed__11;
 static lean_object* l_Lean_IR_EmitC_getDecl___closed__1;
 static lean_object* l_Lean_IR_EmitC_emitInitFn___closed__1;
 lean_object* l_Lean_IR_Decl_normalizeIds(lean_object*);
@@ -1881,56 +1878,28 @@ return x_1;
 static lean_object* _init_l_Lean_IR_EmitC_shouldExport___closed__8() {
 _start:
 {
-lean_object* x_1; 
-x_1 = lean_mk_string_unchecked("Watchdog", 8, 8);
-return x_1;
-}
-}
-static lean_object* _init_l_Lean_IR_EmitC_shouldExport___closed__9() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_IR_EmitC_shouldExport___closed__1;
-x_2 = l_Lean_IR_EmitC_shouldExport___closed__7;
-x_3 = l_Lean_IR_EmitC_shouldExport___closed__8;
-x_4 = l_Lean_Name_mkStr3(x_1, x_2, x_3);
-return x_4;
-}
-}
-static lean_object* _init_l_Lean_IR_EmitC_shouldExport___closed__10() {
-_start:
-{
-lean_object* x_1; 
-x_1 = lean_mk_string_unchecked("ImportCompletion", 16, 16);
-return x_1;
-}
-}
-static lean_object* _init_l_Lean_IR_EmitC_shouldExport___closed__11() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_IR_EmitC_shouldExport___closed__1;
 x_2 = l_Lean_IR_EmitC_shouldExport___closed__7;
-x_3 = l_Lean_IR_EmitC_shouldExport___closed__10;
-x_4 = l_Lean_Name_mkStr3(x_1, x_2, x_3);
-return x_4;
+x_3 = l_Lean_Name_mkStr2(x_1, x_2);
+return x_3;
 }
 }
-static lean_object* _init_l_Lean_IR_EmitC_shouldExport___closed__12() {
+static lean_object* _init_l_Lean_IR_EmitC_shouldExport___closed__9() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string_unchecked("Completion", 10, 10);
+x_1 = lean_mk_string_unchecked("findModuleRefs", 14, 14);
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_IR_EmitC_shouldExport___closed__13() {
+static lean_object* _init_l_Lean_IR_EmitC_shouldExport___closed__10() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_1 = l_Lean_IR_EmitC_shouldExport___closed__1;
 x_2 = l_Lean_IR_EmitC_shouldExport___closed__7;
-x_3 = l_Lean_IR_EmitC_shouldExport___closed__12;
+x_3 = l_Lean_IR_EmitC_shouldExport___closed__9;
 x_4 = l_Lean_Name_mkStr3(x_1, x_2, x_3);
 return x_4;
 }
@@ -1949,57 +1918,34 @@ x_5 = l_Lean_Name_isPrefixOf(x_4, x_1);
 if (x_5 == 0)
 {
 lean_object* x_6; uint8_t x_7; 
-x_6 = l_Lean_IR_EmitC_shouldExport___closed__9;
+x_6 = l_Lean_IR_EmitC_shouldExport___closed__8;
 x_7 = l_Lean_Name_isPrefixOf(x_6, x_1);
 if (x_7 == 0)
 {
-lean_object* x_8; uint8_t x_9; 
-x_8 = l_Lean_IR_EmitC_shouldExport___closed__11;
-x_9 = l_Lean_Name_isPrefixOf(x_8, x_1);
-if (x_9 == 0)
-{
-lean_object* x_10; uint8_t x_11; 
-x_10 = l_Lean_IR_EmitC_shouldExport___closed__13;
-x_11 = l_Lean_Name_isPrefixOf(x_10, x_1);
-if (x_11 == 0)
-{
-uint8_t x_12; 
-x_12 = 1;
-return x_12;
-}
-else
-{
-uint8_t x_13; 
-x_13 = 0;
-return x_13;
-}
-}
-else
-{
-uint8_t x_14; 
-x_14 = 0;
-return x_14;
-}
+uint8_t x_8; 
+x_8 = 1;
+return x_8;
 }
 else
 {
-uint8_t x_15; 
-x_15 = 0;
-return x_15;
+lean_object* x_9; uint8_t x_10; 
+x_9 = l_Lean_IR_EmitC_shouldExport___closed__10;
+x_10 = lean_name_eq(x_1, x_9);
+return x_10;
 }
 }
 else
 {
-uint8_t x_16; 
-x_16 = 0;
-return x_16;
+uint8_t x_11; 
+x_11 = 0;
+return x_11;
 }
 }
 else
 {
-uint8_t x_17; 
-x_17 = 0;
-return x_17;
+uint8_t x_12; 
+x_12 = 0;
+return x_12;
 }
 }
 }
@@ -15888,12 +15834,6 @@ l_Lean_IR_EmitC_shouldExport___closed__9 = _init_l_Lean_IR_EmitC_shouldExport___
 lean_mark_persistent(l_Lean_IR_EmitC_shouldExport___closed__9);
 l_Lean_IR_EmitC_shouldExport___closed__10 = _init_l_Lean_IR_EmitC_shouldExport___closed__10();
 lean_mark_persistent(l_Lean_IR_EmitC_shouldExport___closed__10);
-l_Lean_IR_EmitC_shouldExport___closed__11 = _init_l_Lean_IR_EmitC_shouldExport___closed__11();
-lean_mark_persistent(l_Lean_IR_EmitC_shouldExport___closed__11);
-l_Lean_IR_EmitC_shouldExport___closed__12 = _init_l_Lean_IR_EmitC_shouldExport___closed__12();
-lean_mark_persistent(l_Lean_IR_EmitC_shouldExport___closed__12);
-l_Lean_IR_EmitC_shouldExport___closed__13 = _init_l_Lean_IR_EmitC_shouldExport___closed__13();
-lean_mark_persistent(l_Lean_IR_EmitC_shouldExport___closed__13);
 l_Nat_forM_loop___at_Lean_IR_EmitC_emitFnDeclAux___spec__1___closed__1 = _init_l_Nat_forM_loop___at_Lean_IR_EmitC_emitFnDeclAux___spec__1___closed__1();
 lean_mark_persistent(l_Nat_forM_loop___at_Lean_IR_EmitC_emitFnDeclAux___spec__1___closed__1);
 l_Lean_IR_EmitC_emitFnDeclAux___lambda__1___closed__1 = _init_l_Lean_IR_EmitC_emitFnDeclAux___lambda__1___closed__1();
diff --git a/stage0/stdlib/Std.c b/stage0/stdlib/Std.c
index 8dc2487ff2c2..5ac3a2c843f4 100644
--- a/stage0/stdlib/Std.c
+++ b/stage0/stdlib/Std.c
@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Std
-// Imports: Std.Data Std.Sat
+// Imports: Std.Data
 #include <lean/lean.h>
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@@ -14,7 +14,6 @@
 extern "C" {
 #endif
 lean_object* initialize_Std_Data(uint8_t builtin, lean_object*);
-lean_object* initialize_Std_Sat(uint8_t builtin, lean_object*);
 static bool _G_initialized = false;
 LEAN_EXPORT lean_object* initialize_Std(uint8_t builtin, lean_object* w) {
 lean_object * res;
@@ -23,9 +22,6 @@ _G_initialized = true;
 res = initialize_Std_Data(builtin, lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
-res = initialize_Std_Sat(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
 return lean_io_result_mk_ok(lean_box(0));
 }
 #ifdef __cplusplus
diff --git a/stage0/stdlib/Std/Sat.c b/stage0/stdlib/Std/Sat.c
deleted file mode 100644
index 1b779bd20164..000000000000
--- a/stage0/stdlib/Std/Sat.c
+++ /dev/null
@@ -1,29 +0,0 @@
-// Lean compiler output
-// Module: Std.Sat
-// Imports: Std.Sat.CNF
-#include <lean/lean.h>
-#if defined(__clang__)
-#pragma clang diagnostic ignored "-Wunused-parameter"
-#pragma clang diagnostic ignored "-Wunused-label"
-#elif defined(__GNUC__) && !defined(__CLANG__)
-#pragma GCC diagnostic ignored "-Wunused-parameter"
-#pragma GCC diagnostic ignored "-Wunused-label"
-#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
-#endif
-#ifdef __cplusplus
-extern "C" {
-#endif
-lean_object* initialize_Std_Sat_CNF(uint8_t builtin, lean_object*);
-static bool _G_initialized = false;
-LEAN_EXPORT lean_object* initialize_Std_Sat(uint8_t builtin, lean_object* w) {
-lean_object * res;
-if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
-_G_initialized = true;
-res = initialize_Std_Sat_CNF(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
-return lean_io_result_mk_ok(lean_box(0));
-}
-#ifdef __cplusplus
-}
-#endif
diff --git a/stage0/stdlib/Std/Sat/CNF.c b/stage0/stdlib/Std/Sat/CNF.c
deleted file mode 100644
index 50fc8f94eded..000000000000
--- a/stage0/stdlib/Std/Sat/CNF.c
+++ /dev/null
@@ -1,41 +0,0 @@
-// Lean compiler output
-// Module: Std.Sat.CNF
-// Imports: Std.Sat.CNF.Basic Std.Sat.CNF.Literal Std.Sat.CNF.Relabel Std.Sat.CNF.RelabelFin
-#include <lean/lean.h>
-#if defined(__clang__)
-#pragma clang diagnostic ignored "-Wunused-parameter"
-#pragma clang diagnostic ignored "-Wunused-label"
-#elif defined(__GNUC__) && !defined(__CLANG__)
-#pragma GCC diagnostic ignored "-Wunused-parameter"
-#pragma GCC diagnostic ignored "-Wunused-label"
-#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
-#endif
-#ifdef __cplusplus
-extern "C" {
-#endif
-lean_object* initialize_Std_Sat_CNF_Basic(uint8_t builtin, lean_object*);
-lean_object* initialize_Std_Sat_CNF_Literal(uint8_t builtin, lean_object*);
-lean_object* initialize_Std_Sat_CNF_Relabel(uint8_t builtin, lean_object*);
-lean_object* initialize_Std_Sat_CNF_RelabelFin(uint8_t builtin, lean_object*);
-static bool _G_initialized = false;
-LEAN_EXPORT lean_object* initialize_Std_Sat_CNF(uint8_t builtin, lean_object* w) {
-lean_object * res;
-if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
-_G_initialized = true;
-res = initialize_Std_Sat_CNF_Basic(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
-res = initialize_Std_Sat_CNF_Literal(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
-res = initialize_Std_Sat_CNF_Relabel(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
-res = initialize_Std_Sat_CNF_RelabelFin(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
-return lean_io_result_mk_ok(lean_box(0));
-}
-#ifdef __cplusplus
-}
-#endif
diff --git a/stage0/stdlib/Std/Sat/CNF/Basic.c b/stage0/stdlib/Std/Sat/CNF/Basic.c
deleted file mode 100644
index 6ec78330eb5a..000000000000
--- a/stage0/stdlib/Std/Sat/CNF/Basic.c
+++ /dev/null
@@ -1,362 +0,0 @@
-// Lean compiler output
-// Module: Std.Sat.CNF.Basic
-// Imports: Init.Data.List.Lemmas Init.Data.List.Impl Std.Sat.CNF.Literal
-#include <lean/lean.h>
-#if defined(__clang__)
-#pragma clang diagnostic ignored "-Wunused-parameter"
-#pragma clang diagnostic ignored "-Wunused-label"
-#elif defined(__GNUC__) && !defined(__CLANG__)
-#pragma GCC diagnostic ignored "-Wunused-parameter"
-#pragma GCC diagnostic ignored "-Wunused-label"
-#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
-#endif
-#ifdef __cplusplus
-extern "C" {
-#endif
-LEAN_EXPORT uint8_t l_Std_Sat_CNF_instDecidableExistsMemOfDecidableEq___rarg___lambda__1(lean_object*);
-lean_object* l_instBEqOfDecidableEq___rarg(lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_Clause_instDecidableMemOfDecidableEq___rarg___boxed(lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT uint8_t l_Std_Sat_CNF_Clause_instDecidableMemOfDecidableEq___rarg(lean_object*, lean_object*, lean_object*);
-uint8_t l_List_all___rarg(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_eval___rarg___boxed(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_eval(lean_object*);
-uint8_t l_List_any___rarg(lean_object*, lean_object*);
-LEAN_EXPORT uint8_t l_Std_Sat_CNF_Clause_eval___rarg(lean_object*, lean_object*);
-lean_object* l_instBEqProd___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT uint8_t l_Std_Sat_CNF_Clause_eval___rarg___lambda__1(lean_object*, lean_object*);
-static lean_object* l_Std_Sat_CNF_Clause_instDecidableMemOfDecidableEq___rarg___closed__2;
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_instDecidableMemOfDecidableEq___rarg___boxed(lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_Clause_eval___rarg___lambda__1___boxed(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_instDecidableExistsMemOfDecidableEq___rarg___boxed(lean_object*, lean_object*);
-uint8_t l_List_isEmpty___rarg(lean_object*);
-lean_object* l_instDecidableEqBool___boxed(lean_object*, lean_object*);
-LEAN_EXPORT uint8_t l_Std_Sat_CNF_instDecidableMemOfDecidableEq___rarg(lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_Clause_eval___rarg___boxed(lean_object*, lean_object*);
-uint8_t l_List_elem___rarg(lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT uint8_t l_Std_Sat_CNF_instDecidableMemOfDecidableEq___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
-static lean_object* l_Std_Sat_CNF_Clause_instDecidableMemOfDecidableEq___rarg___closed__1;
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_Clause_instDecidableMemOfDecidableEq(lean_object*);
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_instDecidableExistsMemOfDecidableEq___rarg___lambda__1___boxed(lean_object*);
-LEAN_EXPORT uint8_t l_Std_Sat_CNF_eval___rarg(lean_object*, lean_object*);
-uint8_t l_List_decidableBEx___rarg(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_Clause_eval(lean_object*);
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_instDecidableMemOfDecidableEq(lean_object*);
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_instDecidableExistsMemOfDecidableEq(lean_object*);
-LEAN_EXPORT uint8_t l_Std_Sat_CNF_instDecidableExistsMemOfDecidableEq___rarg(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_instDecidableMemOfDecidableEq___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
-static lean_object* l_Std_Sat_CNF_instDecidableExistsMemOfDecidableEq___rarg___closed__1;
-LEAN_EXPORT uint8_t l_Std_Sat_CNF_Clause_eval___rarg___lambda__1(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-lean_object* x_3; lean_object* x_4; lean_object* x_5; uint8_t x_6; 
-x_3 = lean_ctor_get(x_2, 0);
-lean_inc(x_3);
-x_4 = lean_ctor_get(x_2, 1);
-lean_inc(x_4);
-lean_dec(x_2);
-x_5 = lean_apply_1(x_1, x_3);
-x_6 = lean_unbox(x_5);
-lean_dec(x_5);
-if (x_6 == 0)
-{
-uint8_t x_7; 
-x_7 = lean_unbox(x_4);
-lean_dec(x_4);
-if (x_7 == 0)
-{
-uint8_t x_8; 
-x_8 = 1;
-return x_8;
-}
-else
-{
-uint8_t x_9; 
-x_9 = 0;
-return x_9;
-}
-}
-else
-{
-uint8_t x_10; 
-x_10 = lean_unbox(x_4);
-lean_dec(x_4);
-return x_10;
-}
-}
-}
-LEAN_EXPORT uint8_t l_Std_Sat_CNF_Clause_eval___rarg(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-lean_object* x_3; uint8_t x_4; 
-x_3 = lean_alloc_closure((void*)(l_Std_Sat_CNF_Clause_eval___rarg___lambda__1___boxed), 2, 1);
-lean_closure_set(x_3, 0, x_1);
-x_4 = l_List_any___rarg(x_2, x_3);
-return x_4;
-}
-}
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_Clause_eval(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; 
-x_2 = lean_alloc_closure((void*)(l_Std_Sat_CNF_Clause_eval___rarg___boxed), 2, 0);
-return x_2;
-}
-}
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_Clause_eval___rarg___lambda__1___boxed(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-uint8_t x_3; lean_object* x_4; 
-x_3 = l_Std_Sat_CNF_Clause_eval___rarg___lambda__1(x_1, x_2);
-x_4 = lean_box(x_3);
-return x_4;
-}
-}
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_Clause_eval___rarg___boxed(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-uint8_t x_3; lean_object* x_4; 
-x_3 = l_Std_Sat_CNF_Clause_eval___rarg(x_1, x_2);
-x_4 = lean_box(x_3);
-return x_4;
-}
-}
-LEAN_EXPORT uint8_t l_Std_Sat_CNF_eval___rarg(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-lean_object* x_3; uint8_t x_4; 
-x_3 = lean_alloc_closure((void*)(l_Std_Sat_CNF_Clause_eval___rarg___boxed), 2, 1);
-lean_closure_set(x_3, 0, x_1);
-x_4 = l_List_all___rarg(x_2, x_3);
-return x_4;
-}
-}
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_eval(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; 
-x_2 = lean_alloc_closure((void*)(l_Std_Sat_CNF_eval___rarg___boxed), 2, 0);
-return x_2;
-}
-}
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_eval___rarg___boxed(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-uint8_t x_3; lean_object* x_4; 
-x_3 = l_Std_Sat_CNF_eval___rarg(x_1, x_2);
-x_4 = lean_box(x_3);
-return x_4;
-}
-}
-static lean_object* _init_l_Std_Sat_CNF_Clause_instDecidableMemOfDecidableEq___rarg___closed__1() {
-_start:
-{
-lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_instDecidableEqBool___boxed), 2, 0);
-return x_1;
-}
-}
-static lean_object* _init_l_Std_Sat_CNF_Clause_instDecidableMemOfDecidableEq___rarg___closed__2() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; 
-x_1 = l_Std_Sat_CNF_Clause_instDecidableMemOfDecidableEq___rarg___closed__1;
-x_2 = lean_alloc_closure((void*)(l_instBEqOfDecidableEq___rarg), 3, 1);
-lean_closure_set(x_2, 0, x_1);
-return x_2;
-}
-}
-LEAN_EXPORT uint8_t l_Std_Sat_CNF_Clause_instDecidableMemOfDecidableEq___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
-_start:
-{
-lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10; 
-x_4 = lean_alloc_closure((void*)(l_instBEqOfDecidableEq___rarg), 3, 1);
-lean_closure_set(x_4, 0, x_3);
-x_5 = l_Std_Sat_CNF_Clause_instDecidableMemOfDecidableEq___rarg___closed__2;
-x_6 = lean_alloc_closure((void*)(l_instBEqProd___rarg), 4, 2);
-lean_closure_set(x_6, 0, x_4);
-lean_closure_set(x_6, 1, x_5);
-x_7 = 0;
-x_8 = lean_box(x_7);
-lean_inc(x_1);
-x_9 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_9, 0, x_1);
-lean_ctor_set(x_9, 1, x_8);
-lean_inc(x_2);
-lean_inc(x_6);
-x_10 = l_List_elem___rarg(x_6, x_9, x_2);
-if (x_10 == 0)
-{
-uint8_t x_11; lean_object* x_12; lean_object* x_13; uint8_t x_14; 
-x_11 = 1;
-x_12 = lean_box(x_11);
-x_13 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_13, 0, x_1);
-lean_ctor_set(x_13, 1, x_12);
-x_14 = l_List_elem___rarg(x_6, x_13, x_2);
-return x_14;
-}
-else
-{
-uint8_t x_15; 
-lean_dec(x_6);
-lean_dec(x_2);
-lean_dec(x_1);
-x_15 = 1;
-return x_15;
-}
-}
-}
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_Clause_instDecidableMemOfDecidableEq(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; 
-x_2 = lean_alloc_closure((void*)(l_Std_Sat_CNF_Clause_instDecidableMemOfDecidableEq___rarg___boxed), 3, 0);
-return x_2;
-}
-}
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_Clause_instDecidableMemOfDecidableEq___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
-_start:
-{
-uint8_t x_4; lean_object* x_5; 
-x_4 = l_Std_Sat_CNF_Clause_instDecidableMemOfDecidableEq___rarg(x_1, x_2, x_3);
-x_5 = lean_box(x_4);
-return x_5;
-}
-}
-LEAN_EXPORT uint8_t l_Std_Sat_CNF_instDecidableMemOfDecidableEq___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
-_start:
-{
-uint8_t x_4; 
-x_4 = l_Std_Sat_CNF_Clause_instDecidableMemOfDecidableEq___rarg(x_1, x_3, x_2);
-return x_4;
-}
-}
-LEAN_EXPORT uint8_t l_Std_Sat_CNF_instDecidableMemOfDecidableEq___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
-_start:
-{
-lean_object* x_4; uint8_t x_5; 
-x_4 = lean_alloc_closure((void*)(l_Std_Sat_CNF_instDecidableMemOfDecidableEq___rarg___lambda__1___boxed), 3, 2);
-lean_closure_set(x_4, 0, x_1);
-lean_closure_set(x_4, 1, x_3);
-x_5 = l_List_decidableBEx___rarg(x_4, x_2);
-return x_5;
-}
-}
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_instDecidableMemOfDecidableEq(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; 
-x_2 = lean_alloc_closure((void*)(l_Std_Sat_CNF_instDecidableMemOfDecidableEq___rarg___boxed), 3, 0);
-return x_2;
-}
-}
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_instDecidableMemOfDecidableEq___rarg___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
-_start:
-{
-uint8_t x_4; lean_object* x_5; 
-x_4 = l_Std_Sat_CNF_instDecidableMemOfDecidableEq___rarg___lambda__1(x_1, x_2, x_3);
-x_5 = lean_box(x_4);
-return x_5;
-}
-}
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_instDecidableMemOfDecidableEq___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
-_start:
-{
-uint8_t x_4; lean_object* x_5; 
-x_4 = l_Std_Sat_CNF_instDecidableMemOfDecidableEq___rarg(x_1, x_2, x_3);
-x_5 = lean_box(x_4);
-return x_5;
-}
-}
-LEAN_EXPORT uint8_t l_Std_Sat_CNF_instDecidableExistsMemOfDecidableEq___rarg___lambda__1(lean_object* x_1) {
-_start:
-{
-uint8_t x_2; 
-x_2 = l_List_isEmpty___rarg(x_1);
-if (x_2 == 0)
-{
-uint8_t x_3; 
-x_3 = 1;
-return x_3;
-}
-else
-{
-uint8_t x_4; 
-x_4 = 0;
-return x_4;
-}
-}
-}
-static lean_object* _init_l_Std_Sat_CNF_instDecidableExistsMemOfDecidableEq___rarg___closed__1() {
-_start:
-{
-lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_Std_Sat_CNF_instDecidableExistsMemOfDecidableEq___rarg___lambda__1___boxed), 1, 0);
-return x_1;
-}
-}
-LEAN_EXPORT uint8_t l_Std_Sat_CNF_instDecidableExistsMemOfDecidableEq___rarg(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-lean_object* x_3; uint8_t x_4; 
-x_3 = l_Std_Sat_CNF_instDecidableExistsMemOfDecidableEq___rarg___closed__1;
-x_4 = l_List_any___rarg(x_1, x_3);
-return x_4;
-}
-}
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_instDecidableExistsMemOfDecidableEq(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; 
-x_2 = lean_alloc_closure((void*)(l_Std_Sat_CNF_instDecidableExistsMemOfDecidableEq___rarg___boxed), 2, 0);
-return x_2;
-}
-}
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_instDecidableExistsMemOfDecidableEq___rarg___lambda__1___boxed(lean_object* x_1) {
-_start:
-{
-uint8_t x_2; lean_object* x_3; 
-x_2 = l_Std_Sat_CNF_instDecidableExistsMemOfDecidableEq___rarg___lambda__1(x_1);
-lean_dec(x_1);
-x_3 = lean_box(x_2);
-return x_3;
-}
-}
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_instDecidableExistsMemOfDecidableEq___rarg___boxed(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-uint8_t x_3; lean_object* x_4; 
-x_3 = l_Std_Sat_CNF_instDecidableExistsMemOfDecidableEq___rarg(x_1, x_2);
-lean_dec(x_2);
-x_4 = lean_box(x_3);
-return x_4;
-}
-}
-lean_object* initialize_Init_Data_List_Lemmas(uint8_t builtin, lean_object*);
-lean_object* initialize_Init_Data_List_Impl(uint8_t builtin, lean_object*);
-lean_object* initialize_Std_Sat_CNF_Literal(uint8_t builtin, lean_object*);
-static bool _G_initialized = false;
-LEAN_EXPORT lean_object* initialize_Std_Sat_CNF_Basic(uint8_t builtin, lean_object* w) {
-lean_object * res;
-if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
-_G_initialized = true;
-res = initialize_Init_Data_List_Lemmas(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
-res = initialize_Init_Data_List_Impl(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
-res = initialize_Std_Sat_CNF_Literal(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
-l_Std_Sat_CNF_Clause_instDecidableMemOfDecidableEq___rarg___closed__1 = _init_l_Std_Sat_CNF_Clause_instDecidableMemOfDecidableEq___rarg___closed__1();
-lean_mark_persistent(l_Std_Sat_CNF_Clause_instDecidableMemOfDecidableEq___rarg___closed__1);
-l_Std_Sat_CNF_Clause_instDecidableMemOfDecidableEq___rarg___closed__2 = _init_l_Std_Sat_CNF_Clause_instDecidableMemOfDecidableEq___rarg___closed__2();
-lean_mark_persistent(l_Std_Sat_CNF_Clause_instDecidableMemOfDecidableEq___rarg___closed__2);
-l_Std_Sat_CNF_instDecidableExistsMemOfDecidableEq___rarg___closed__1 = _init_l_Std_Sat_CNF_instDecidableExistsMemOfDecidableEq___rarg___closed__1();
-lean_mark_persistent(l_Std_Sat_CNF_instDecidableExistsMemOfDecidableEq___rarg___closed__1);
-return lean_io_result_mk_ok(lean_box(0));
-}
-#ifdef __cplusplus
-}
-#endif
diff --git a/stage0/stdlib/Std/Sat/CNF/Literal.c b/stage0/stdlib/Std/Sat/CNF/Literal.c
deleted file mode 100644
index 6a4acad434d1..000000000000
--- a/stage0/stdlib/Std/Sat/CNF/Literal.c
+++ /dev/null
@@ -1,179 +0,0 @@
-// Lean compiler output
-// Module: Std.Sat.CNF.Literal
-// Imports: Init.Data.Hashable Init.Data.ToString
-#include <lean/lean.h>
-#if defined(__clang__)
-#pragma clang diagnostic ignored "-Wunused-parameter"
-#pragma clang diagnostic ignored "-Wunused-label"
-#elif defined(__GNUC__) && !defined(__CLANG__)
-#pragma GCC diagnostic ignored "-Wunused-parameter"
-#pragma GCC diagnostic ignored "-Wunused-label"
-#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
-#endif
-#ifdef __cplusplus
-extern "C" {
-#endif
-static lean_object* l_Std_Sat_Literal_dimacs___rarg___closed__1;
-static lean_object* l_Std_Sat_Literal_dimacs___rarg___closed__2;
-LEAN_EXPORT lean_object* l_Std_Sat_Literal_dimacs___rarg(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Std_Sat_Literal_negate(lean_object*);
-LEAN_EXPORT lean_object* l_Std_Sat_Literal_negate___rarg(lean_object*);
-lean_object* lean_string_append(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Std_Sat_Literal_dimacs(lean_object*);
-LEAN_EXPORT lean_object* l_Std_Sat_Literal_negate___rarg(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; uint8_t x_3; 
-x_2 = lean_ctor_get(x_1, 1);
-lean_inc(x_2);
-x_3 = lean_unbox(x_2);
-lean_dec(x_2);
-if (x_3 == 0)
-{
-uint8_t x_4; 
-x_4 = !lean_is_exclusive(x_1);
-if (x_4 == 0)
-{
-lean_object* x_5; uint8_t x_6; lean_object* x_7; 
-x_5 = lean_ctor_get(x_1, 1);
-lean_dec(x_5);
-x_6 = 1;
-x_7 = lean_box(x_6);
-lean_ctor_set(x_1, 1, x_7);
-return x_1;
-}
-else
-{
-lean_object* x_8; uint8_t x_9; lean_object* x_10; lean_object* x_11; 
-x_8 = lean_ctor_get(x_1, 0);
-lean_inc(x_8);
-lean_dec(x_1);
-x_9 = 1;
-x_10 = lean_box(x_9);
-x_11 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_11, 0, x_8);
-lean_ctor_set(x_11, 1, x_10);
-return x_11;
-}
-}
-else
-{
-uint8_t x_12; 
-x_12 = !lean_is_exclusive(x_1);
-if (x_12 == 0)
-{
-lean_object* x_13; uint8_t x_14; lean_object* x_15; 
-x_13 = lean_ctor_get(x_1, 1);
-lean_dec(x_13);
-x_14 = 0;
-x_15 = lean_box(x_14);
-lean_ctor_set(x_1, 1, x_15);
-return x_1;
-}
-else
-{
-lean_object* x_16; uint8_t x_17; lean_object* x_18; lean_object* x_19; 
-x_16 = lean_ctor_get(x_1, 0);
-lean_inc(x_16);
-lean_dec(x_1);
-x_17 = 0;
-x_18 = lean_box(x_17);
-x_19 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_19, 0, x_16);
-lean_ctor_set(x_19, 1, x_18);
-return x_19;
-}
-}
-}
-}
-LEAN_EXPORT lean_object* l_Std_Sat_Literal_negate(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; 
-x_2 = lean_alloc_closure((void*)(l_Std_Sat_Literal_negate___rarg), 1, 0);
-return x_2;
-}
-}
-static lean_object* _init_l_Std_Sat_Literal_dimacs___rarg___closed__1() {
-_start:
-{
-lean_object* x_1; 
-x_1 = lean_mk_string_unchecked("-", 1, 1);
-return x_1;
-}
-}
-static lean_object* _init_l_Std_Sat_Literal_dimacs___rarg___closed__2() {
-_start:
-{
-lean_object* x_1; 
-x_1 = lean_mk_string_unchecked("", 0, 0);
-return x_1;
-}
-}
-LEAN_EXPORT lean_object* l_Std_Sat_Literal_dimacs___rarg(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-lean_object* x_3; uint8_t x_4; 
-x_3 = lean_ctor_get(x_2, 1);
-lean_inc(x_3);
-x_4 = lean_unbox(x_3);
-lean_dec(x_3);
-if (x_4 == 0)
-{
-lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; 
-x_5 = lean_ctor_get(x_2, 0);
-lean_inc(x_5);
-lean_dec(x_2);
-x_6 = lean_apply_1(x_1, x_5);
-x_7 = l_Std_Sat_Literal_dimacs___rarg___closed__1;
-x_8 = lean_string_append(x_7, x_6);
-lean_dec(x_6);
-x_9 = l_Std_Sat_Literal_dimacs___rarg___closed__2;
-x_10 = lean_string_append(x_8, x_9);
-return x_10;
-}
-else
-{
-lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; 
-x_11 = lean_ctor_get(x_2, 0);
-lean_inc(x_11);
-lean_dec(x_2);
-x_12 = lean_apply_1(x_1, x_11);
-x_13 = l_Std_Sat_Literal_dimacs___rarg___closed__2;
-x_14 = lean_string_append(x_13, x_12);
-lean_dec(x_12);
-x_15 = lean_string_append(x_14, x_13);
-return x_15;
-}
-}
-}
-LEAN_EXPORT lean_object* l_Std_Sat_Literal_dimacs(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; 
-x_2 = lean_alloc_closure((void*)(l_Std_Sat_Literal_dimacs___rarg), 2, 0);
-return x_2;
-}
-}
-lean_object* initialize_Init_Data_Hashable(uint8_t builtin, lean_object*);
-lean_object* initialize_Init_Data_ToString(uint8_t builtin, lean_object*);
-static bool _G_initialized = false;
-LEAN_EXPORT lean_object* initialize_Std_Sat_CNF_Literal(uint8_t builtin, lean_object* w) {
-lean_object * res;
-if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
-_G_initialized = true;
-res = initialize_Init_Data_Hashable(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
-res = initialize_Init_Data_ToString(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
-l_Std_Sat_Literal_dimacs___rarg___closed__1 = _init_l_Std_Sat_Literal_dimacs___rarg___closed__1();
-lean_mark_persistent(l_Std_Sat_Literal_dimacs___rarg___closed__1);
-l_Std_Sat_Literal_dimacs___rarg___closed__2 = _init_l_Std_Sat_Literal_dimacs___rarg___closed__2();
-lean_mark_persistent(l_Std_Sat_Literal_dimacs___rarg___closed__2);
-return lean_io_result_mk_ok(lean_box(0));
-}
-#ifdef __cplusplus
-}
-#endif
diff --git a/stage0/stdlib/Std/Sat/CNF/Relabel.c b/stage0/stdlib/Std/Sat/CNF/Relabel.c
deleted file mode 100644
index 1c293c22b849..000000000000
--- a/stage0/stdlib/Std/Sat/CNF/Relabel.c
+++ /dev/null
@@ -1,239 +0,0 @@
-// Lean compiler output
-// Module: Std.Sat.CNF.Relabel
-// Imports: Std.Sat.CNF.Basic
-#include <lean/lean.h>
-#if defined(__clang__)
-#pragma clang diagnostic ignored "-Wunused-parameter"
-#pragma clang diagnostic ignored "-Wunused-label"
-#elif defined(__GNUC__) && !defined(__CLANG__)
-#pragma GCC diagnostic ignored "-Wunused-parameter"
-#pragma GCC diagnostic ignored "-Wunused-label"
-#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
-#endif
-#ifdef __cplusplus
-extern "C" {
-#endif
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_relabel(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_List_mapTR_loop___at_Std_Sat_CNF_Clause_relabel___spec__1(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_List_mapTR_loop___at_Std_Sat_CNF_Clause_relabel___spec__1___rarg(lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_relabel___rarg(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_List_mapTR_loop___at_Std_Sat_CNF_relabel___spec__1___rarg(lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_Clause_relabel___rarg(lean_object*, lean_object*);
-lean_object* l_List_reverse___rarg(lean_object*);
-LEAN_EXPORT lean_object* l_List_mapTR_loop___at_Std_Sat_CNF_relabel___spec__1(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_Clause_relabel(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_List_mapTR_loop___at_Std_Sat_CNF_Clause_relabel___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
-_start:
-{
-if (lean_obj_tag(x_2) == 0)
-{
-lean_object* x_4; 
-lean_dec(x_1);
-x_4 = l_List_reverse___rarg(x_3);
-return x_4;
-}
-else
-{
-uint8_t x_5; 
-x_5 = !lean_is_exclusive(x_2);
-if (x_5 == 0)
-{
-lean_object* x_6; uint8_t x_7; 
-x_6 = lean_ctor_get(x_2, 0);
-x_7 = !lean_is_exclusive(x_6);
-if (x_7 == 0)
-{
-lean_object* x_8; lean_object* x_9; lean_object* x_10; 
-x_8 = lean_ctor_get(x_2, 1);
-x_9 = lean_ctor_get(x_6, 0);
-lean_inc(x_1);
-x_10 = lean_apply_1(x_1, x_9);
-lean_ctor_set(x_6, 0, x_10);
-lean_ctor_set(x_2, 1, x_3);
-{
-lean_object* _tmp_1 = x_8;
-lean_object* _tmp_2 = x_2;
-x_2 = _tmp_1;
-x_3 = _tmp_2;
-}
-goto _start;
-}
-else
-{
-lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; 
-x_12 = lean_ctor_get(x_2, 1);
-x_13 = lean_ctor_get(x_6, 0);
-x_14 = lean_ctor_get(x_6, 1);
-lean_inc(x_14);
-lean_inc(x_13);
-lean_dec(x_6);
-lean_inc(x_1);
-x_15 = lean_apply_1(x_1, x_13);
-x_16 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_16, 0, x_15);
-lean_ctor_set(x_16, 1, x_14);
-lean_ctor_set(x_2, 1, x_3);
-lean_ctor_set(x_2, 0, x_16);
-{
-lean_object* _tmp_1 = x_12;
-lean_object* _tmp_2 = x_2;
-x_2 = _tmp_1;
-x_3 = _tmp_2;
-}
-goto _start;
-}
-}
-else
-{
-lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; 
-x_18 = lean_ctor_get(x_2, 0);
-x_19 = lean_ctor_get(x_2, 1);
-lean_inc(x_19);
-lean_inc(x_18);
-lean_dec(x_2);
-x_20 = lean_ctor_get(x_18, 0);
-lean_inc(x_20);
-x_21 = lean_ctor_get(x_18, 1);
-lean_inc(x_21);
-if (lean_is_exclusive(x_18)) {
- lean_ctor_release(x_18, 0);
- lean_ctor_release(x_18, 1);
- x_22 = x_18;
-} else {
- lean_dec_ref(x_18);
- x_22 = lean_box(0);
-}
-lean_inc(x_1);
-x_23 = lean_apply_1(x_1, x_20);
-if (lean_is_scalar(x_22)) {
- x_24 = lean_alloc_ctor(0, 2, 0);
-} else {
- x_24 = x_22;
-}
-lean_ctor_set(x_24, 0, x_23);
-lean_ctor_set(x_24, 1, x_21);
-x_25 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_25, 0, x_24);
-lean_ctor_set(x_25, 1, x_3);
-x_2 = x_19;
-x_3 = x_25;
-goto _start;
-}
-}
-}
-}
-LEAN_EXPORT lean_object* l_List_mapTR_loop___at_Std_Sat_CNF_Clause_relabel___spec__1(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-lean_object* x_3; 
-x_3 = lean_alloc_closure((void*)(l_List_mapTR_loop___at_Std_Sat_CNF_Clause_relabel___spec__1___rarg), 3, 0);
-return x_3;
-}
-}
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_Clause_relabel___rarg(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-lean_object* x_3; lean_object* x_4; 
-x_3 = lean_box(0);
-x_4 = l_List_mapTR_loop___at_Std_Sat_CNF_Clause_relabel___spec__1___rarg(x_1, x_2, x_3);
-return x_4;
-}
-}
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_Clause_relabel(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-lean_object* x_3; 
-x_3 = lean_alloc_closure((void*)(l_Std_Sat_CNF_Clause_relabel___rarg), 2, 0);
-return x_3;
-}
-}
-LEAN_EXPORT lean_object* l_List_mapTR_loop___at_Std_Sat_CNF_relabel___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
-_start:
-{
-if (lean_obj_tag(x_2) == 0)
-{
-lean_object* x_4; 
-lean_dec(x_1);
-x_4 = l_List_reverse___rarg(x_3);
-return x_4;
-}
-else
-{
-uint8_t x_5; 
-x_5 = !lean_is_exclusive(x_2);
-if (x_5 == 0)
-{
-lean_object* x_6; lean_object* x_7; lean_object* x_8; 
-x_6 = lean_ctor_get(x_2, 0);
-x_7 = lean_ctor_get(x_2, 1);
-lean_inc(x_1);
-x_8 = l_Std_Sat_CNF_Clause_relabel___rarg(x_1, x_6);
-lean_ctor_set(x_2, 1, x_3);
-lean_ctor_set(x_2, 0, x_8);
-{
-lean_object* _tmp_1 = x_7;
-lean_object* _tmp_2 = x_2;
-x_2 = _tmp_1;
-x_3 = _tmp_2;
-}
-goto _start;
-}
-else
-{
-lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; 
-x_10 = lean_ctor_get(x_2, 0);
-x_11 = lean_ctor_get(x_2, 1);
-lean_inc(x_11);
-lean_inc(x_10);
-lean_dec(x_2);
-lean_inc(x_1);
-x_12 = l_Std_Sat_CNF_Clause_relabel___rarg(x_1, x_10);
-x_13 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_13, 0, x_12);
-lean_ctor_set(x_13, 1, x_3);
-x_2 = x_11;
-x_3 = x_13;
-goto _start;
-}
-}
-}
-}
-LEAN_EXPORT lean_object* l_List_mapTR_loop___at_Std_Sat_CNF_relabel___spec__1(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-lean_object* x_3; 
-x_3 = lean_alloc_closure((void*)(l_List_mapTR_loop___at_Std_Sat_CNF_relabel___spec__1___rarg), 3, 0);
-return x_3;
-}
-}
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_relabel___rarg(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-lean_object* x_3; lean_object* x_4; 
-x_3 = lean_box(0);
-x_4 = l_List_mapTR_loop___at_Std_Sat_CNF_relabel___spec__1___rarg(x_1, x_2, x_3);
-return x_4;
-}
-}
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_relabel(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-lean_object* x_3; 
-x_3 = lean_alloc_closure((void*)(l_Std_Sat_CNF_relabel___rarg), 2, 0);
-return x_3;
-}
-}
-lean_object* initialize_Std_Sat_CNF_Basic(uint8_t builtin, lean_object*);
-static bool _G_initialized = false;
-LEAN_EXPORT lean_object* initialize_Std_Sat_CNF_Relabel(uint8_t builtin, lean_object* w) {
-lean_object * res;
-if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
-_G_initialized = true;
-res = initialize_Std_Sat_CNF_Basic(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
-return lean_io_result_mk_ok(lean_box(0));
-}
-#ifdef __cplusplus
-}
-#endif
diff --git a/stage0/stdlib/Std/Sat/CNF/RelabelFin.c b/stage0/stdlib/Std/Sat/CNF/RelabelFin.c
deleted file mode 100644
index 4eb8144990ab..000000000000
--- a/stage0/stdlib/Std/Sat/CNF/RelabelFin.c
+++ /dev/null
@@ -1,380 +0,0 @@
-// Lean compiler output
-// Module: Std.Sat.CNF.RelabelFin
-// Imports: Init.Data.List.Nat.Basic Std.Sat.CNF.Relabel
-#include <lean/lean.h>
-#if defined(__clang__)
-#pragma clang diagnostic ignored "-Wunused-parameter"
-#pragma clang diagnostic ignored "-Wunused-label"
-#elif defined(__GNUC__) && !defined(__CLANG__)
-#pragma GCC diagnostic ignored "-Wunused-parameter"
-#pragma GCC diagnostic ignored "-Wunused-label"
-#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
-#endif
-#ifdef __cplusplus
-extern "C" {
-#endif
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_relabelFin___lambda__1(lean_object*, lean_object*);
-lean_object* lean_mk_empty_array_with_capacity(lean_object*);
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_relabelFin___lambda__1___boxed(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_relabelFin(lean_object*);
-lean_object* lean_array_push(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_List_foldl___at_Std_Sat_CNF_Clause_maxLiteral___spec__3___boxed(lean_object*, lean_object*);
-lean_object* l_Std_Sat_CNF_relabel___rarg(lean_object*, lean_object*);
-uint8_t l_List_any___rarg(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l___private_Std_Sat_CNF_RelabelFin_0__Std_Sat_CNF_numLiterals_match__1_splitter(lean_object*);
-static lean_object* l_Std_Sat_CNF_relabelFin___closed__1;
-LEAN_EXPORT lean_object* l___private_Std_Sat_CNF_RelabelFin_0__Std_Sat_CNF_numLiterals_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_List_maximum_x3f___at_Std_Sat_CNF_Clause_maxLiteral___spec__2(lean_object*);
-lean_object* lean_array_to_list(lean_object*, lean_object*);
-static lean_object* l_Std_Sat_CNF_maxLiteral___closed__1;
-lean_object* l_List_replicateTR___rarg(lean_object*, lean_object*);
-lean_object* l_List_lengthTRAux___rarg(lean_object*, lean_object*);
-lean_object* l_Std_Sat_CNF_instDecidableExistsMemOfDecidableEq___rarg___lambda__1___boxed(lean_object*);
-LEAN_EXPORT lean_object* l_List_maximum_x3f___at_Std_Sat_CNF_Clause_maxLiteral___spec__2___boxed(lean_object*);
-uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_Clause_maxLiteral(lean_object*);
-LEAN_EXPORT lean_object* l_List_mapTR_loop___at_Std_Sat_CNF_Clause_maxLiteral___spec__1(lean_object*, lean_object*);
-lean_object* l_List_reverse___rarg(lean_object*);
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_maxLiteral(lean_object*);
-LEAN_EXPORT lean_object* l_List_foldl___at_Std_Sat_CNF_Clause_maxLiteral___spec__3(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_numLiterals(lean_object*);
-uint8_t lean_nat_dec_le(lean_object*, lean_object*);
-lean_object* lean_nat_add(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_List_filterMapTR_go___at_Std_Sat_CNF_maxLiteral___spec__1(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l___private_Std_Sat_CNF_RelabelFin_0__Std_Sat_CNF_numLiterals_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_List_mapTR_loop___at_Std_Sat_CNF_Clause_maxLiteral___spec__1(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-if (lean_obj_tag(x_1) == 0)
-{
-lean_object* x_3; 
-x_3 = l_List_reverse___rarg(x_2);
-return x_3;
-}
-else
-{
-uint8_t x_4; 
-x_4 = !lean_is_exclusive(x_1);
-if (x_4 == 0)
-{
-lean_object* x_5; lean_object* x_6; lean_object* x_7; 
-x_5 = lean_ctor_get(x_1, 0);
-x_6 = lean_ctor_get(x_1, 1);
-x_7 = lean_ctor_get(x_5, 0);
-lean_inc(x_7);
-lean_dec(x_5);
-lean_ctor_set(x_1, 1, x_2);
-lean_ctor_set(x_1, 0, x_7);
-{
-lean_object* _tmp_0 = x_6;
-lean_object* _tmp_1 = x_1;
-x_1 = _tmp_0;
-x_2 = _tmp_1;
-}
-goto _start;
-}
-else
-{
-lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; 
-x_9 = lean_ctor_get(x_1, 0);
-x_10 = lean_ctor_get(x_1, 1);
-lean_inc(x_10);
-lean_inc(x_9);
-lean_dec(x_1);
-x_11 = lean_ctor_get(x_9, 0);
-lean_inc(x_11);
-lean_dec(x_9);
-x_12 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_12, 0, x_11);
-lean_ctor_set(x_12, 1, x_2);
-x_1 = x_10;
-x_2 = x_12;
-goto _start;
-}
-}
-}
-}
-LEAN_EXPORT lean_object* l_List_foldl___at_Std_Sat_CNF_Clause_maxLiteral___spec__3(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-if (lean_obj_tag(x_2) == 0)
-{
-lean_inc(x_1);
-return x_1;
-}
-else
-{
-lean_object* x_3; lean_object* x_4; uint8_t x_5; 
-x_3 = lean_ctor_get(x_2, 0);
-x_4 = lean_ctor_get(x_2, 1);
-x_5 = lean_nat_dec_le(x_1, x_3);
-if (x_5 == 0)
-{
-x_2 = x_4;
-goto _start;
-}
-else
-{
-x_1 = x_3;
-x_2 = x_4;
-goto _start;
-}
-}
-}
-}
-LEAN_EXPORT lean_object* l_List_maximum_x3f___at_Std_Sat_CNF_Clause_maxLiteral___spec__2(lean_object* x_1) {
-_start:
-{
-if (lean_obj_tag(x_1) == 0)
-{
-lean_object* x_2; 
-x_2 = lean_box(0);
-return x_2;
-}
-else
-{
-lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
-x_3 = lean_ctor_get(x_1, 0);
-x_4 = lean_ctor_get(x_1, 1);
-x_5 = l_List_foldl___at_Std_Sat_CNF_Clause_maxLiteral___spec__3(x_3, x_4);
-x_6 = lean_alloc_ctor(1, 1, 0);
-lean_ctor_set(x_6, 0, x_5);
-return x_6;
-}
-}
-}
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_Clause_maxLiteral(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_2 = lean_box(0);
-x_3 = l_List_mapTR_loop___at_Std_Sat_CNF_Clause_maxLiteral___spec__1(x_1, x_2);
-x_4 = l_List_maximum_x3f___at_Std_Sat_CNF_Clause_maxLiteral___spec__2(x_3);
-lean_dec(x_3);
-return x_4;
-}
-}
-LEAN_EXPORT lean_object* l_List_foldl___at_Std_Sat_CNF_Clause_maxLiteral___spec__3___boxed(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-lean_object* x_3; 
-x_3 = l_List_foldl___at_Std_Sat_CNF_Clause_maxLiteral___spec__3(x_1, x_2);
-lean_dec(x_2);
-lean_dec(x_1);
-return x_3;
-}
-}
-LEAN_EXPORT lean_object* l_List_maximum_x3f___at_Std_Sat_CNF_Clause_maxLiteral___spec__2___boxed(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; 
-x_2 = l_List_maximum_x3f___at_Std_Sat_CNF_Clause_maxLiteral___spec__2(x_1);
-lean_dec(x_1);
-return x_2;
-}
-}
-LEAN_EXPORT lean_object* l_List_filterMapTR_go___at_Std_Sat_CNF_maxLiteral___spec__1(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-if (lean_obj_tag(x_1) == 0)
-{
-lean_object* x_3; 
-x_3 = lean_array_to_list(lean_box(0), x_2);
-return x_3;
-}
-else
-{
-lean_object* x_4; lean_object* x_5; lean_object* x_6; 
-x_4 = lean_ctor_get(x_1, 0);
-lean_inc(x_4);
-x_5 = lean_ctor_get(x_1, 1);
-lean_inc(x_5);
-lean_dec(x_1);
-x_6 = l_Std_Sat_CNF_Clause_maxLiteral(x_4);
-if (lean_obj_tag(x_6) == 0)
-{
-x_1 = x_5;
-goto _start;
-}
-else
-{
-lean_object* x_8; lean_object* x_9; 
-x_8 = lean_ctor_get(x_6, 0);
-lean_inc(x_8);
-lean_dec(x_6);
-x_9 = lean_array_push(x_2, x_8);
-x_1 = x_5;
-x_2 = x_9;
-goto _start;
-}
-}
-}
-}
-static lean_object* _init_l_Std_Sat_CNF_maxLiteral___closed__1() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; 
-x_1 = lean_unsigned_to_nat(0u);
-x_2 = lean_mk_empty_array_with_capacity(x_1);
-return x_2;
-}
-}
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_maxLiteral(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_2 = l_Std_Sat_CNF_maxLiteral___closed__1;
-x_3 = l_List_filterMapTR_go___at_Std_Sat_CNF_maxLiteral___spec__1(x_1, x_2);
-x_4 = l_List_maximum_x3f___at_Std_Sat_CNF_Clause_maxLiteral___spec__2(x_3);
-lean_dec(x_3);
-return x_4;
-}
-}
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_numLiterals(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; 
-x_2 = l_Std_Sat_CNF_maxLiteral(x_1);
-if (lean_obj_tag(x_2) == 0)
-{
-lean_object* x_3; 
-x_3 = lean_unsigned_to_nat(0u);
-return x_3;
-}
-else
-{
-lean_object* x_4; lean_object* x_5; lean_object* x_6; 
-x_4 = lean_ctor_get(x_2, 0);
-lean_inc(x_4);
-lean_dec(x_2);
-x_5 = lean_unsigned_to_nat(1u);
-x_6 = lean_nat_add(x_4, x_5);
-lean_dec(x_4);
-return x_6;
-}
-}
-}
-LEAN_EXPORT lean_object* l___private_Std_Sat_CNF_RelabelFin_0__Std_Sat_CNF_numLiterals_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
-_start:
-{
-if (lean_obj_tag(x_1) == 0)
-{
-lean_dec(x_3);
-lean_inc(x_2);
-return x_2;
-}
-else
-{
-lean_object* x_4; lean_object* x_5; 
-x_4 = lean_ctor_get(x_1, 0);
-lean_inc(x_4);
-lean_dec(x_1);
-x_5 = lean_apply_1(x_3, x_4);
-return x_5;
-}
-}
-}
-LEAN_EXPORT lean_object* l___private_Std_Sat_CNF_RelabelFin_0__Std_Sat_CNF_numLiterals_match__1_splitter(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; 
-x_2 = lean_alloc_closure((void*)(l___private_Std_Sat_CNF_RelabelFin_0__Std_Sat_CNF_numLiterals_match__1_splitter___rarg___boxed), 3, 0);
-return x_2;
-}
-}
-LEAN_EXPORT lean_object* l___private_Std_Sat_CNF_RelabelFin_0__Std_Sat_CNF_numLiterals_match__1_splitter___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
-_start:
-{
-lean_object* x_4; 
-x_4 = l___private_Std_Sat_CNF_RelabelFin_0__Std_Sat_CNF_numLiterals_match__1_splitter___rarg(x_1, x_2, x_3);
-lean_dec(x_2);
-return x_4;
-}
-}
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_relabelFin___lambda__1(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-uint8_t x_3; 
-x_3 = lean_nat_dec_lt(x_2, x_1);
-if (x_3 == 0)
-{
-lean_object* x_4; 
-x_4 = lean_unsigned_to_nat(0u);
-return x_4;
-}
-else
-{
-lean_inc(x_2);
-return x_2;
-}
-}
-}
-static lean_object* _init_l_Std_Sat_CNF_relabelFin___closed__1() {
-_start:
-{
-lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_Std_Sat_CNF_instDecidableExistsMemOfDecidableEq___rarg___lambda__1___boxed), 1, 0);
-return x_1;
-}
-}
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_relabelFin(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; uint8_t x_3; 
-x_2 = l_Std_Sat_CNF_relabelFin___closed__1;
-lean_inc(x_1);
-x_3 = l_List_any___rarg(x_1, x_2);
-if (x_3 == 0)
-{
-lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
-x_4 = lean_unsigned_to_nat(0u);
-x_5 = l_List_lengthTRAux___rarg(x_1, x_4);
-lean_dec(x_1);
-x_6 = lean_box(0);
-x_7 = l_List_replicateTR___rarg(x_5, x_6);
-return x_7;
-}
-else
-{
-lean_object* x_8; lean_object* x_9; lean_object* x_10; 
-lean_inc(x_1);
-x_8 = l_Std_Sat_CNF_numLiterals(x_1);
-x_9 = lean_alloc_closure((void*)(l_Std_Sat_CNF_relabelFin___lambda__1___boxed), 2, 1);
-lean_closure_set(x_9, 0, x_8);
-x_10 = l_Std_Sat_CNF_relabel___rarg(x_9, x_1);
-return x_10;
-}
-}
-}
-LEAN_EXPORT lean_object* l_Std_Sat_CNF_relabelFin___lambda__1___boxed(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-lean_object* x_3; 
-x_3 = l_Std_Sat_CNF_relabelFin___lambda__1(x_1, x_2);
-lean_dec(x_2);
-lean_dec(x_1);
-return x_3;
-}
-}
-lean_object* initialize_Init_Data_List_Nat_Basic(uint8_t builtin, lean_object*);
-lean_object* initialize_Std_Sat_CNF_Relabel(uint8_t builtin, lean_object*);
-static bool _G_initialized = false;
-LEAN_EXPORT lean_object* initialize_Std_Sat_CNF_RelabelFin(uint8_t builtin, lean_object* w) {
-lean_object * res;
-if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
-_G_initialized = true;
-res = initialize_Init_Data_List_Nat_Basic(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
-res = initialize_Std_Sat_CNF_Relabel(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
-l_Std_Sat_CNF_maxLiteral___closed__1 = _init_l_Std_Sat_CNF_maxLiteral___closed__1();
-lean_mark_persistent(l_Std_Sat_CNF_maxLiteral___closed__1);
-l_Std_Sat_CNF_relabelFin___closed__1 = _init_l_Std_Sat_CNF_relabelFin___closed__1();
-lean_mark_persistent(l_Std_Sat_CNF_relabelFin___closed__1);
-return lean_io_result_mk_ok(lean_box(0));
-}
-#ifdef __cplusplus
-}
-#endif