remove useless comment

fblanqui · fblanqui · commit e7dde4c15cd2 · 2021-03-23T15:52:00.000+01:00
diff --git a/Nat.lp b/Nat.lp
@@ -9,8 +9,6 @@ inductive ℕ : TYPE ≔
 constant symbol nat : Set;
 
 rule τ nat ↪ ℕ;
-//unif_rule τ $x ≡ ℕ ↪ [ $x ≡ nat ];
-// FIXME: should be infered from the injectivity of τ
 
 // Enabling the use of decimal notation
 
