nelim fixed

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / nat.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/nat.ma b/helm/software/matita/contribs/ng_assembly/freescale/nat.ma
index aacc7b1dd26f3d0d398751ee25ba661ccaa854e7..4753b4cac745c482654b4547ed63bae7c15bfe64 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/nat.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/nat.ma
@@ -37,15 +37,6 @@ default "natural numbers" cic:/matita/freescale/nat/nat.ind.
 
 alias num (instance 0) = "natural number".
 
-nlet rec nat_ind (P:nat → Prop) (p:P O) (f:Πn:nat.P n → P (S n)) (n:nat) on n : P n ≝
- match n with [ O ⇒ p | S (n1:nat) ⇒ f n1 (nat_ind P p f n1) ].
-
-nlet rec nat_rec (P:nat → Set) (p:P O) (f:Πn:nat.P n → P (S n)) (n:nat) on n : P n ≝
- match n with [ O ⇒ p | S (n1:nat) ⇒ f n1 (nat_rec P p f n1) ].
-
-nlet rec nat_rect (P:nat → Type) (p:P O) (f:Πn:nat.P n → P (S n)) (n:nat) on n : P n ≝
- match n with [ O ⇒ p | S (n1:nat) ⇒ f n1 (nat_rect P p f n1) ].
-
 nlet rec eq_nat (n1,n2:nat) on n1 ≝
  match n1 with
   [ O ⇒ match n2 with [ O ⇒ true | S _ ⇒ false ]