Procedural : tentative update to the new letin cic construction

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / LambdaDelta-1 / next_plus / props.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/props.ma
index 41139d520e3d38690ddc72fd5691d980b42a7668..7e26f27a7f902769562d09c93f0d75d4fefb044f 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/props.ma
@@ -14,9 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/next_plus/props".
-
-include "next_plus/defs.ma".
+include "LambdaDelta-1/next_plus/defs.ma".
 
 theorem next_plus_assoc:
  \forall (g: G).(\forall (n: nat).(\forall (h1: nat).(\forall (h2: nat).(eq 
@@ -52,11 +50,10 @@ theorem next_plus_lt:
 g n) h))))
 \def
  \lambda (g: G).(\lambda (h: nat).(nat_ind (\lambda (n: nat).(\forall (n0: 
-nat).(lt n0 (next_plus g (next g n0) n)))) (\lambda (n: nat).(le_S_n (S n) 
-(next g n) (lt_le_S (S n) (S (next g n)) (lt_n_S n (next g n) (next_lt g 
-n))))) (\lambda (n: nat).(\lambda (H: ((\forall (n0: nat).(lt n0 (next_plus g 
-(next g n0) n))))).(\lambda (n0: nat).(eq_ind nat (next_plus g (next g (next 
-g n0)) n) (\lambda (n1: nat).(lt n0 n1)) (lt_trans n0 (next g n0) (next_plus 
-g (next g (next g n0)) n) (next_lt g n0) (H (next g n0))) (next g (next_plus 
-g (next g n0) n)) (next_plus_next g (next g n0) n))))) h)).
+nat).(lt n0 (next_plus g (next g n0) n)))) (\lambda (n: nat).(next_lt g n)) 
+(\lambda (n: nat).(\lambda (H: ((\forall (n0: nat).(lt n0 (next_plus g (next 
+g n0) n))))).(\lambda (n0: nat).(eq_ind nat (next_plus g (next g (next g n0)) 
+n) (\lambda (n1: nat).(lt n0 n1)) (lt_trans n0 (next g n0) (next_plus g (next 
+g (next g n0)) n) (next_lt g n0) (H (next g n0))) (next g (next_plus g (next 
+g n0) n)) (next_plus_next g (next g n0) n))))) h)).