diff --git a/paper/rat.lp b/paper/rat.lp
index c0a20bf49c7d93a0915fa84b816b72c40c5797aa..a64cde3198325f64407165d4b78791f06c2e624a 100644
--- a/paper/rat.lp
+++ b/paper/rat.lp
@@ -79,7 +79,7 @@ proof
   refine snd (Snz n)
   assume n Hn
   refine nznat_induction
-           (λz, (Z =ℕ (fst (Snz n) * (fst z))) ⊃ false) ?zOnz[n,Hn] ?zSnz[n,Hn]
+           (λz, (Z =ℕ (fst (Snz n) * (fst z))) ⊃ false) ?zOnz[n;Hn] ?zSnz[n;Hn]
   simpl
   refine snd (Snz n)
   assume m Hm
diff --git a/prelude/numbers.lp b/prelude/numbers.lp
index 28d32a6d58e5b910048c0a8eb10915339fe92b56..d0ead4eb595fed52060f947ef8a5e4371f44cd4e 100644
--- a/prelude/numbers.lp
+++ b/prelude/numbers.lp
@@ -49,15 +49,15 @@ symbol associative_add
 constant symbol real_pred: η (pred numfield)
 definition real ≔ psub real_pred
 
-set flag "print_implicits" on
 symbol Num_real: ε (∀ (λx: η {|!Number!|}, real_pred (insertnum x)))
 
 // Built in the PVS typechecker
 
-definition nonzero_real ≔
-  psub {real}
-       (λx: η real,
-        neq {_} x (cast {_} {real} (λx, x) (insertnum 0) _))
+// TODO: metavariables left
+// definition nonzero_real ≔
+//   psub {real}
+//        (λx: η real,
+//         neq {_} x (cast {_} {real} (λx, x) (insertnum 0) _))
 
 // symbol closed_plus_real: Π(x y: Term real),
 //   let pr ≔ S.restr numfield real_pred in