X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fty3%2Farity_props.ma;h=b831585162c933d56e187f8bb2ca897b56a5d839;hb=6329f0f87906d3347c39d2ba2f5ec2b2124f17a2;hp=0e221591c485dd0cb6fac0cffee44d383c0902d0;hpb=783fbc6eb42d5db260d93d8d213a7d5c035e99e3;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity_props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity_props.ma
index 0e221591c..b83158516 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity_props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity_props.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-
+set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/arity_props".
 
 include "ty3/arity.ma".
 
@@ -29,29 +29,27 @@ Prop).P)))))))
 \def
  \lambda (g: G).(\lambda (c: C).(\lambda (v: T).(\lambda (t: T).(\lambda (u: 
 T).(\lambda (H: (ty3 g c (THead (Bind Abst) v t) u)).(\lambda (H0: (pc3 c u 
-v)).(\lambda (P: Prop).(let H1 \def H in (ex4_3_ind T T T (\lambda (t2: 
-T).(\lambda (_: T).(\lambda (_: T).(pc3 c (THead (Bind Abst) v t2) u)))) 
-(\lambda (_: T).(\lambda (t0: T).(\lambda (_: T).(ty3 g c v t0)))) (\lambda 
-(t2: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) v) t 
-t2)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (t1: T).(ty3 g (CHead c 
-(Bind Abst) v) t2 t1)))) P (\lambda (x0: T).(\lambda (x1: T).(\lambda (x2: 
-T).(\lambda (_: (pc3 c (THead (Bind Abst) v x0) u)).(\lambda (H3: (ty3 g c v 
-x1)).(\lambda (_: (ty3 g (CHead c (Bind Abst) v) t x0)).(\lambda (_: (ty3 g 
-(CHead c (Bind Abst) v) x0 x2)).(let H_y \def (ty3_conv g c v x1 H3 (THead 
-(Bind Abst) v t) u H H0) in (let H_x \def (ty3_arity g c (THead (Bind Abst) v 
-t) v H_y) in (let H6 \def H_x in (ex2_ind A (\lambda (a1: A).(arity g c 
-(THead (Bind Abst) v t) a1)) (\lambda (a1: A).(arity g c v (asucc g a1))) P 
-(\lambda (x: A).(\lambda (H7: (arity g c (THead (Bind Abst) v t) x)).(\lambda 
-(H8: (arity g c v (asucc g x))).(let H9 \def (arity_gen_abst g c v t x H7) in 
-(ex3_2_ind A A (\lambda (a1: A).(\lambda (a2: A).(eq A x (AHead a1 a2)))) 
-(\lambda (a1: A).(\lambda (_: A).(arity g c v (asucc g a1)))) (\lambda (_: 
-A).(\lambda (a2: A).(arity g (CHead c (Bind Abst) v) t a2))) P (\lambda (x3: 
-A).(\lambda (x4: A).(\lambda (H10: (eq A x (AHead x3 x4))).(\lambda (H11: 
-(arity g c v (asucc g x3))).(\lambda (_: (arity g (CHead c (Bind Abst) v) t 
-x4)).(let H13 \def (eq_ind A x (\lambda (a: A).(arity g c v (asucc g a))) H8 
-(AHead x3 x4) H10) in (leq_ahead_asucc_false g x3 (asucc g x4) (arity_mono g 
-c v (asucc g (AHead x3 x4)) H13 (asucc g x3) H11) P))))))) H9))))) 
-H6))))))))))) (ty3_gen_bind g Abst c v t u H1)))))))))).
+v)).(\lambda (P: Prop).(let H1 \def H in (ex3_2_ind T T (\lambda (t2: 
+T).(\lambda (_: T).(pc3 c (THead (Bind Abst) v t2) u))) (\lambda (_: 
+T).(\lambda (t0: T).(ty3 g c v t0))) (\lambda (t2: T).(\lambda (_: T).(ty3 g 
+(CHead c (Bind Abst) v) t t2))) P (\lambda (x0: T).(\lambda (x1: T).(\lambda 
+(_: (pc3 c (THead (Bind Abst) v x0) u)).(\lambda (H3: (ty3 g c v 
+x1)).(\lambda (_: (ty3 g (CHead c (Bind Abst) v) t x0)).(let H_y \def 
+(ty3_conv g c v x1 H3 (THead (Bind Abst) v t) u H H0) in (let H_x \def 
+(ty3_arity g c (THead (Bind Abst) v t) v H_y) in (let H5 \def H_x in (ex2_ind 
+A (\lambda (a1: A).(arity g c (THead (Bind Abst) v t) a1)) (\lambda (a1: 
+A).(arity g c v (asucc g a1))) P (\lambda (x: A).(\lambda (H6: (arity g c 
+(THead (Bind Abst) v t) x)).(\lambda (H7: (arity g c v (asucc g x))).(let H8 
+\def (arity_gen_abst g c v t x H6) in (ex3_2_ind A A (\lambda (a1: 
+A).(\lambda (a2: A).(eq A x (AHead a1 a2)))) (\lambda (a1: A).(\lambda (_: 
+A).(arity g c v (asucc g a1)))) (\lambda (_: A).(\lambda (a2: A).(arity g 
+(CHead c (Bind Abst) v) t a2))) P (\lambda (x2: A).(\lambda (x3: A).(\lambda 
+(H9: (eq A x (AHead x2 x3))).(\lambda (H10: (arity g c v (asucc g 
+x2))).(\lambda (_: (arity g (CHead c (Bind Abst) v) t x3)).(let H12 \def 
+(eq_ind A x (\lambda (a: A).(arity g c v (asucc g a))) H7 (AHead x2 x3) H9) 
+in (leq_ahead_asucc_false g x2 (asucc g x3) (arity_mono g c v (asucc g (AHead 
+x2 x3)) H12 (asucc g x2) H10) P))))))) H8))))) H5))))))))) (ty3_gen_bind g 
+Abst c v t u H1)))))))))).
 
 theorem ty3_repellent:
  \forall (g: G).(\forall (c: C).(\forall (w: T).(\forall (t: T).(\forall (u1: