X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fpr2%2Fprops.ma;h=8b11644d3e3fdaf731d86149bf6bc787cd9b1377;hb=d0982534aee06a30f91a06d2f3e82834b132a3d3;hp=2f8498c59635daf6b48e119c3cb12571b226ed13;hpb=5c1b44dfefa085fbb56e23047652d3650be9d855;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/props.ma
index 2f8498c59..8b11644d3 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/props.ma
@@ -14,8 +14,6 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-
-
 include "pr2/defs.ma".
 
 include "pr0/props.ma".
@@ -241,29 +239,29 @@ T).(\forall (t1: T).(\forall (t2: T).((pr2 (CHead c (Bind b) v1) t1 t2) \to
  \lambda (b: B).(\lambda (H: (not (eq B b Abbr))).(\lambda (c: C).(\lambda 
 (v1: T).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H0: (pr2 (CHead c (Bind 
 b) v1) t1 t2)).(\lambda (v2: T).(insert_eq C (CHead c (Bind b) v1) (\lambda 
-(c0: C).(pr2 c0 t1 t2)) (pr2 (CHead c (Bind b) v2) t1 t2) (\lambda (y: 
-C).(\lambda (H1: (pr2 y t1 t2)).(pr2_ind (\lambda (c0: C).(\lambda (t: 
-T).(\lambda (t0: T).((eq C c0 (CHead c (Bind b) v1)) \to (pr2 (CHead c (Bind 
-b) v2) t t0))))) (\lambda (c0: C).(\lambda (t3: T).(\lambda (t4: T).(\lambda 
-(H2: (pr0 t3 t4)).(\lambda (_: (eq C c0 (CHead c (Bind b) v1))).(pr2_free 
-(CHead c (Bind b) v2) t3 t4 H2)))))) (\lambda (c0: C).(\lambda (d: 
-C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H2: (getl i c0 (CHead d (Bind 
-Abbr) u))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H3: (pr0 t3 
-t4)).(\lambda (t: T).(\lambda (H4: (subst0 i u t4 t)).(\lambda (H5: (eq C c0 
-(CHead c (Bind b) v1))).(let H6 \def (eq_ind C c0 (\lambda (c1: C).(getl i c1 
-(CHead d (Bind Abbr) u))) H2 (CHead c (Bind b) v1) H5) in (nat_ind (\lambda 
-(n: nat).((getl n (CHead c (Bind b) v1) (CHead d (Bind Abbr) u)) \to ((subst0 
-n u t4 t) \to (pr2 (CHead c (Bind b) v2) t3 t)))) (\lambda (H7: (getl O 
-(CHead c (Bind b) v1) (CHead d (Bind Abbr) u))).(\lambda (H8: (subst0 O u t4 
-t)).(let H9 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda 
-(_: C).C) with [(CSort _) \Rightarrow d | (CHead c1 _ _) \Rightarrow c1])) 
-(CHead d (Bind Abbr) u) (CHead c (Bind b) v1) (clear_gen_bind b c (CHead d 
-(Bind Abbr) u) v1 (getl_gen_O (CHead c (Bind b) v1) (CHead d (Bind Abbr) u) 
-H7))) in ((let H10 \def (f_equal C B (\lambda (e: C).(match e in C return 
-(\lambda (_: C).B) with [(CSort _) \Rightarrow Abbr | (CHead _ k _) 
-\Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b0) 
-\Rightarrow b0 | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u) 
-(CHead c (Bind b) v1) (clear_gen_bind b c (CHead d (Bind Abbr) u) v1 
+(c0: C).(pr2 c0 t1 t2)) (\lambda (_: C).(pr2 (CHead c (Bind b) v2) t1 t2)) 
+(\lambda (y: C).(\lambda (H1: (pr2 y t1 t2)).(pr2_ind (\lambda (c0: 
+C).(\lambda (t: T).(\lambda (t0: T).((eq C c0 (CHead c (Bind b) v1)) \to (pr2 
+(CHead c (Bind b) v2) t t0))))) (\lambda (c0: C).(\lambda (t3: T).(\lambda 
+(t4: T).(\lambda (H2: (pr0 t3 t4)).(\lambda (_: (eq C c0 (CHead c (Bind b) 
+v1))).(pr2_free (CHead c (Bind b) v2) t3 t4 H2)))))) (\lambda (c0: 
+C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H2: (getl i c0 
+(CHead d (Bind Abbr) u))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H3: 
+(pr0 t3 t4)).(\lambda (t: T).(\lambda (H4: (subst0 i u t4 t)).(\lambda (H5: 
+(eq C c0 (CHead c (Bind b) v1))).(let H6 \def (eq_ind C c0 (\lambda (c1: 
+C).(getl i c1 (CHead d (Bind Abbr) u))) H2 (CHead c (Bind b) v1) H5) in 
+(nat_ind (\lambda (n: nat).((getl n (CHead c (Bind b) v1) (CHead d (Bind 
+Abbr) u)) \to ((subst0 n u t4 t) \to (pr2 (CHead c (Bind b) v2) t3 t)))) 
+(\lambda (H7: (getl O (CHead c (Bind b) v1) (CHead d (Bind Abbr) 
+u))).(\lambda (H8: (subst0 O u t4 t)).(let H9 \def (f_equal C C (\lambda (e: 
+C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d | 
+(CHead c1 _ _) \Rightarrow c1])) (CHead d (Bind Abbr) u) (CHead c (Bind b) 
+v1) (clear_gen_bind b c (CHead d (Bind Abbr) u) v1 (getl_gen_O (CHead c (Bind 
+b) v1) (CHead d (Bind Abbr) u) H7))) in ((let H10 \def (f_equal C B (\lambda 
+(e: C).(match e in C return (\lambda (_: C).B) with [(CSort _) \Rightarrow 
+Abbr | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).B) with 
+[(Bind b0) \Rightarrow b0 | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind 
+Abbr) u) (CHead c (Bind b) v1) (clear_gen_bind b c (CHead d (Bind Abbr) u) v1 
 (getl_gen_O (CHead c (Bind b) v1) (CHead d (Bind Abbr) u) H7))) in ((let H11 
 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) 
 with [(CSort _) \Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) (CHead d