splat_args is now better understood and debugged: we need TWO splat_args, one when

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/ty3.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/ty3.ma
index 3fbcb516fe2e9c3221e4c392664fe24809181c06..cc8839f26daff46e6c2f099939d3c62b0f71f1e6 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/ty3.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/ty3.ma
@@ -14,8 +14,6 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/ty3".
-
 include "csubt/pc3.ma".
 
 include "csubt/props.ma".
@@ -70,16 +68,13 @@ T).(\lambda (_: (ty3 g c u t)).(\lambda (H1: ((\forall (c2: C).((csubt g c
 c2) \to (ty3 g c2 u t))))).(\lambda (b: B).(\lambda (t0: T).(\lambda (t3: 
 T).(\lambda (_: (ty3 g (CHead c (Bind b) u) t0 t3)).(\lambda (H3: ((\forall 
 (c2: C).((csubt g (CHead c (Bind b) u) c2) \to (ty3 g c2 t0 t3))))).(\lambda 
-(t4: T).(\lambda (_: (ty3 g (CHead c (Bind b) u) t3 t4)).(\lambda (H5: 
-((\forall (c2: C).((csubt g (CHead c (Bind b) u) c2) \to (ty3 g c2 t3 
-t4))))).(\lambda (c2: C).(\lambda (H6: (csubt g c c2)).(ty3_bind g c2 u t (H1 
-c2 H6) b t0 t3 (H3 (CHead c2 (Bind b) u) (csubt_head g c c2 H6 (Bind b) u)) 
-t4 (H5 (CHead c2 (Bind b) u) (csubt_head g c c2 H6 (Bind b) 
-u)))))))))))))))))) (\lambda (c: C).(\lambda (w: T).(\lambda (u: T).(\lambda 
-(_: (ty3 g c w u)).(\lambda (H1: ((\forall (c2: C).((csubt g c c2) \to (ty3 g 
-c2 w u))))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g c v (THead 
-(Bind Abst) u t))).(\lambda (H3: ((\forall (c2: C).((csubt g c c2) \to (ty3 g 
-c2 v (THead (Bind Abst) u t)))))).(\lambda (c2: C).(\lambda (H4: (csubt g c 
+(c2: C).(\lambda (H4: (csubt g c c2)).(ty3_bind g c2 u t (H1 c2 H4) b t0 t3 
+(H3 (CHead c2 (Bind b) u) (csubt_head g c c2 H4 (Bind b) u))))))))))))))) 
+(\lambda (c: C).(\lambda (w: T).(\lambda (u: T).(\lambda (_: (ty3 g c w 
+u)).(\lambda (H1: ((\forall (c2: C).((csubt g c c2) \to (ty3 g c2 w 
+u))))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g c v (THead (Bind 
+Abst) u t))).(\lambda (H3: ((\forall (c2: C).((csubt g c c2) \to (ty3 g c2 v 
+(THead (Bind Abst) u t)))))).(\lambda (c2: C).(\lambda (H4: (csubt g c 
 c2)).(ty3_appl g c2 w u (H1 c2 H4) v t (H3 c2 H4))))))))))))) (\lambda (c: 
 C).(\lambda (t0: T).(\lambda (t3: T).(\lambda (_: (ty3 g c t0 t3)).(\lambda 
 (H1: ((\forall (c2: C).((csubt g c c2) \to (ty3 g c2 t0 t3))))).(\lambda (t4: