diff --git a/encodings/subtype.lp b/encodings/subtype.lp
index f01d8af4fd320bdab7459107cf913dabd12d7dfa..e6fbe95adc3143eebd96e3c4760631462ef238e9 100644
--- a/encodings/subtype.lp
+++ b/encodings/subtype.lp
@@ -28,8 +28,6 @@ definition ↓ {t} ≔ downcast {t}
 
 // rule η (maxcast (maxcast $t)) ↪ η (maxcast $t)
 
-set flag "print_implicits" on
-set debug +u
 rule π {$t ~> $u} ↪ λx: η $t → η (μ $u), ∀ (λy, π (x y))
 with π {psub {$t} $a}
    ↪ λx: η (μ $t), (π {μ $t} x) ∧ (λy: ε (π {μ $t} x), $a (↓ x y))
@@ -72,7 +70,6 @@ proof
   refine λx: ε false, x
 qed
 
-set flag "print_implicits" on
 rule ε ($t ≃ $t) ↪ ε true
 rule ε (($t1 ~> $u1) ≃ ($t2 ~> $u2))
    ↪ ε ((μ $t1 ≃ μ $t2)
diff --git a/prelude/numbers.lp b/prelude/numbers.lp
index ad0342203ea29824ef4f344a57dd225cd275b635..28d32a6d58e5b910048c0a8eb10915339fe92b56 100644
--- a/prelude/numbers.lp
+++ b/prelude/numbers.lp
@@ -49,7 +49,6 @@ symbol associative_add
 constant symbol real_pred: η (pred numfield)
 definition real ≔ psub real_pred
 
-set debug +u
 set flag "print_implicits" on
 symbol Num_real: ε (∀ (λx: η {|!Number!|}, real_pred (insertnum x)))