equivalence_relations made uniform w.r.t. universe level

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / LambdaDelta-1 / pr3 / iso.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/iso.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/iso.ma
index 7ec0ba521881b330e671f9cd5554723a45a781d3..51e8083d9e21adb395e1948f5dee4d6b60dd0fcb 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/iso.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/iso.ma
@@ -14,13 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
+include "LambdaDelta-1/pr3/fwd.ma".
 
+include "LambdaDelta-1/iso/props.ma".
 
-include "pr3/fwd.ma".
-
-include "iso/props.ma".
-
-include "tlist/props.ma".
+include "LambdaDelta-1/tlist/props.ma".
 
 theorem pr3_iso_appls_abbr:
  \forall (c: C).(\forall (d: C).(\forall (w: T).(\forall (i: nat).((getl i c 
@@ -760,7 +758,7 @@ in (\forall (c: C).(\forall (u2: T).((pr3 c u1 u2) \to ((((iso u1 u2) \to
 (lifts (S O) O vs) t)) u2))))))))))
 \def
  \lambda (b: B).(\lambda (H: (not (eq B b Abst))).(\lambda (vs: 
-TList).(tlist_ind_rew (\lambda (t: TList).(\forall (u: T).(\forall (t0: 
+TList).(tlist_ind_rev (\lambda (t: TList).(\forall (u: T).(\forall (t0: 
 T).(let u1 \def (THeads (Flat Appl) t (THead (Bind b) u t0)) in (\forall (c: 
 C).(\forall (u2: T).((pr3 c u1 u2) \to ((((iso u1 u2) \to (\forall (P: 
 Prop).P))) \to (pr3 c (THead (Bind b) u (THeads (Flat Appl) (lifts (S O) O t) 
@@ -781,11 +779,11 @@ u2)) (eq_ind_r T (THeads (Flat Appl) (lifts (S O) O ts) (THead (Flat Appl)
 (lift (S O) O t) t0)) (\lambda (t1: T).(pr3 c (THead (Bind b) u t1) u2)) (let 
 H3 \def (eq_ind T (THeads (Flat Appl) (TApp ts t) (THead (Bind b) u t0)) 
 (\lambda (t1: T).(pr3 c t1 u2)) H1 (THeads (Flat Appl) ts (THead (Flat Appl) 
-t (THead (Bind b) u t0))) (theads_tapp (Flat Appl) ts t (THead (Bind b) u 
-t0))) in (let H4 \def (eq_ind T (THeads (Flat Appl) (TApp ts t) (THead (Bind 
+t (THead (Bind b) u t0))) (theads_tapp (Flat Appl) t (THead (Bind b) u t0) 
+ts)) in (let H4 \def (eq_ind T (THeads (Flat Appl) (TApp ts t) (THead (Bind 
 b) u t0)) (\lambda (t1: T).((iso t1 u2) \to (\forall (P: Prop).P))) H2 
 (THeads (Flat Appl) ts (THead (Flat Appl) t (THead (Bind b) u t0))) 
-(theads_tapp (Flat Appl) ts t (THead (Bind b) u t0))) in (TList_ind (\lambda 
+(theads_tapp (Flat Appl) t (THead (Bind b) u t0) ts)) in (TList_ind (\lambda 
 (t1: TList).(((\forall (u0: T).(\forall (t2: T).(\forall (c0: C).(\forall 
 (u3: T).((pr3 c0 (THeads (Flat Appl) t1 (THead (Bind b) u0 t2)) u3) \to 
 ((((iso (THeads (Flat Appl) t1 (THead (Bind b) u0 t2)) u3) \to (\forall (P: 
@@ -829,7 +827,7 @@ t) t0))) (iso_head t1 t1 (THeads (Flat Appl) ts0 (THead (Flat Appl) t (THead
 (Bind b) u t0))) (THeads (Flat Appl) ts0 (THead (Bind b) u (THead (Flat Appl) 
 (lift (S O) O t) t0))) (Flat Appl)) u2 H8) P)))))))))) ts H0 H3 H4))) (THeads 
 (Flat Appl) (TApp (lifts (S O) O ts) (lift (S O) O t)) t0) (theads_tapp (Flat 
-Appl) (lifts (S O) O ts) (lift (S O) O t) t0)) (lifts (S O) O (TApp ts t)) 
+Appl) (lift (S O) O t) t0 (lifts (S O) O ts))) (lifts (S O) O (TApp ts t)) 
 (lifts_tapp (S O) O t ts))))))))))) vs))).
 
 theorem pr3_iso_beta: