Procedural : tentative update to the new letin cic construction

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / LambdaDelta-1 / ty3 / pr3_props.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props.ma
index aa574990d257db2c494dcb92fd4b99522f6e01af..20d795000ffb91ead3cb52f2cb02da289405e162 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props.ma
@@ -14,9 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props".
-
-include "ty3/pr3.ma".
+include "LambdaDelta-1/ty3/pr3.ma".
 
 theorem ty3_cred_pr2:
  \forall (g: G).(\forall (c: C).(\forall (v1: T).(\forall (v2: T).((pr2 c v1 
@@ -120,7 +118,7 @@ nat).(\lambda (H4: (eq T (TLRef n) (lift h x1 x0))).(\lambda (e: C).(\lambda
 \def H_x in (or_ind (land (lt n x1) (eq T x0 (TLRef n))) (land (le (plus x1 
 h) n) (eq T x0 (TLRef (minus n h)))) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h 
 x1 t2) (lift (S n) O t))) (\lambda (t2: T).(ty3 g e x0 t2))) (\lambda (H7: 
-(land (lt n x1) (eq T x0 (TLRef n)))).(and_ind (lt n x1) (eq T x0 (TLRef n)) 
+(land (lt n x1) (eq T x0 (TLRef n)))).(land_ind (lt n x1) (eq T x0 (TLRef n)) 
 (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O t))) (\lambda 
 (t2: T).(ty3 g e x0 t2))) (\lambda (H8: (lt n x1)).(\lambda (H9: (eq T x0 
 (TLRef n))).(eq_ind_r T (TLRef n) (\lambda (t0: T).(ex2 T (\lambda (t2: 
@@ -156,7 +154,7 @@ x1 (S n)) x4) t H17) (lift h (plus (S n) (minus x1 (S n))) (lift (S n) O x4))
 n e x3 x2 H12 x4 H18)) x1 (le_plus_minus (S n) x1 H8))))) H16))))))))) 
 (getl_drop_conf_lt Abbr c0 d0 u n H1 e h (minus x1 (S n)) H10))) x0 H9))) 
 H7)) (\lambda (H7: (land (le (plus x1 h) n) (eq T x0 (TLRef (minus n 
-h))))).(and_ind (le (plus x1 h) n) (eq T x0 (TLRef (minus n h))) (ex2 T 
+h))))).(land_ind (le (plus x1 h) n) (eq T x0 (TLRef (minus n h))) (ex2 T 
 (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O t))) (\lambda (t2: 
 T).(ty3 g e x0 t2))) (\lambda (H8: (le (plus x1 h) n)).(\lambda (H9: (eq T x0 
 (TLRef (minus n h)))).(eq_ind_r T (TLRef (minus n h)) (\lambda (t0: T).(ex2 T 
@@ -184,7 +182,7 @@ nat).(\lambda (H4: (eq T (TLRef n) (lift h x1 x0))).(\lambda (e: C).(\lambda
 \def H_x in (or_ind (land (lt n x1) (eq T x0 (TLRef n))) (land (le (plus x1 
 h) n) (eq T x0 (TLRef (minus n h)))) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h 
 x1 t2) (lift (S n) O u))) (\lambda (t2: T).(ty3 g e x0 t2))) (\lambda (H7: 
-(land (lt n x1) (eq T x0 (TLRef n)))).(and_ind (lt n x1) (eq T x0 (TLRef n)) 
+(land (lt n x1) (eq T x0 (TLRef n)))).(land_ind (lt n x1) (eq T x0 (TLRef n)) 
 (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O u))) (\lambda 
 (t2: T).(ty3 g e x0 t2))) (\lambda (H8: (lt n x1)).(\lambda (H9: (eq T x0 
 (TLRef n))).(eq_ind_r T (TLRef n) (\lambda (t0: T).(ex2 T (\lambda (t2: 
@@ -226,7 +224,7 @@ n) (minus x1 (S n))) (lift (S n) O x2)) (lift_d x2 h (S n) (minus x1 (S n)) O
 (le_O_n (minus x1 (S n))))) (ty3_abst g n e x3 x2 H12 x4 H18)) x1 
 (le_plus_minus (S n) x1 H8))))) H16)) u H11)))))))) (getl_drop_conf_lt Abst 
 c0 d0 u n H1 e h (minus x1 (S n)) H10))) x0 H9))) H7)) (\lambda (H7: (land 
-(le (plus x1 h) n) (eq T x0 (TLRef (minus n h))))).(and_ind (le (plus x1 h) 
+(le (plus x1 h) n) (eq T x0 (TLRef (minus n h))))).(land_ind (le (plus x1 h) 
 n) (eq T x0 (TLRef (minus n h))) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 
 t2) (lift (S n) O u))) (\lambda (t2: T).(ty3 g e x0 t2))) (\lambda (H8: (le 
 (plus x1 h) n)).(\lambda (H9: (eq T x0 (TLRef (minus n h)))).(eq_ind_r T