equivalence_relations made uniform w.r.t. universe level

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / LambdaDelta-1 / pr2 / fwd.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/fwd.ma
index c332a5ffbee5070c4f6e43ccccd87231c4a58f2b..fe6666a1d93f4a933d95bddc0f69dbcd08fc8152 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/fwd.ma
@@ -78,21 +78,21 @@ in (eq_ind_r T (TLRef n) (\lambda (t0: T).(or (eq T t t0) (ex2_2 C T (\lambda
 (d0: C).(\lambda (u0: T).(getl n c0 (CHead d0 (Bind Abbr) u0)))) (\lambda (_: 
 C).(\lambda (u0: T).(eq T t (lift (S n) O u0))))))) (let H6 \def (eq_ind T t2 
 (\lambda (t0: T).(subst0 i u t0 t)) H3 (TLRef n) (pr0_gen_lref t2 n H5)) in 
-(and_ind (eq nat n i) (eq T t (lift (S n) O u)) (or (eq T t (TLRef n)) (ex2_2 
-C T (\lambda (d0: C).(\lambda (u0: T).(getl n c0 (CHead d0 (Bind Abbr) u0)))) 
-(\lambda (_: C).(\lambda (u0: T).(eq T t (lift (S n) O u0)))))) (\lambda (H7: 
-(eq nat n i)).(\lambda (H8: (eq T t (lift (S n) O u))).(eq_ind_r T (lift (S 
-n) O u) (\lambda (t0: T).(or (eq T t0 (TLRef n)) (ex2_2 C T (\lambda (d0: 
-C).(\lambda (u0: T).(getl n c0 (CHead d0 (Bind Abbr) u0)))) (\lambda (_: 
-C).(\lambda (u0: T).(eq T t0 (lift (S n) O u0))))))) (let H9 \def (eq_ind_r 
-nat i (\lambda (n0: nat).(getl n0 c0 (CHead d (Bind Abbr) u))) H1 n H7) in 
-(or_intror (eq T (lift (S n) O u) (TLRef n)) (ex2_2 C T (\lambda (d0: 
-C).(\lambda (u0: T).(getl n c0 (CHead d0 (Bind Abbr) u0)))) (\lambda (_: 
-C).(\lambda (u0: T).(eq T (lift (S n) O u) (lift (S n) O u0))))) (ex2_2_intro 
-C T (\lambda (d0: C).(\lambda (u0: T).(getl n c0 (CHead d0 (Bind Abbr) u0)))) 
-(\lambda (_: C).(\lambda (u0: T).(eq T (lift (S n) O u) (lift (S n) O u0)))) 
-d u H9 (refl_equal T (lift (S n) O u))))) t H8))) (subst0_gen_lref u t i n 
-H6))) t1 H4))))))))))))) c y x H0))) H)))).
+(land_ind (eq nat n i) (eq T t (lift (S n) O u)) (or (eq T t (TLRef n)) 
+(ex2_2 C T (\lambda (d0: C).(\lambda (u0: T).(getl n c0 (CHead d0 (Bind Abbr) 
+u0)))) (\lambda (_: C).(\lambda (u0: T).(eq T t (lift (S n) O u0)))))) 
+(\lambda (H7: (eq nat n i)).(\lambda (H8: (eq T t (lift (S n) O 
+u))).(eq_ind_r T (lift (S n) O u) (\lambda (t0: T).(or (eq T t0 (TLRef n)) 
+(ex2_2 C T (\lambda (d0: C).(\lambda (u0: T).(getl n c0 (CHead d0 (Bind Abbr) 
+u0)))) (\lambda (_: C).(\lambda (u0: T).(eq T t0 (lift (S n) O u0))))))) (let 
+H9 \def (eq_ind_r nat i (\lambda (n0: nat).(getl n0 c0 (CHead d (Bind Abbr) 
+u))) H1 n H7) in (or_intror (eq T (lift (S n) O u) (TLRef n)) (ex2_2 C T 
+(\lambda (d0: C).(\lambda (u0: T).(getl n c0 (CHead d0 (Bind Abbr) u0)))) 
+(\lambda (_: C).(\lambda (u0: T).(eq T (lift (S n) O u) (lift (S n) O u0))))) 
+(ex2_2_intro C T (\lambda (d0: C).(\lambda (u0: T).(getl n c0 (CHead d0 (Bind 
+Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(eq T (lift (S n) O u) (lift (S 
+n) O u0)))) d u H9 (refl_equal T (lift (S n) O u))))) t H8))) 
+(subst0_gen_lref u t i n H6))) t1 H4))))))))))))) c y x H0))) H)))).
 
 theorem pr2_gen_abst:
  \forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr2 c