syntax and commenting invalid line

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

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