regeneration with new results

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/fwd.ma
index ef2a4d4d94799e65dee2077c8b4edd0b9c6544f9..fe23589d56585796deac2af4741332a6d4fc0bd7 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/fwd.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-
+set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/clear/fwd".
 
 include "clear/defs.ma".
 
@@ -117,21 +117,21 @@ theorem clear_gen_flat_r:
 \def
  \lambda (f: F).(\lambda (x: C).(\lambda (e: C).(\lambda (u: T).(\lambda (H: 
 (clear x (CHead e (Flat f) u))).(\lambda (P: Prop).(insert_eq C (CHead e 
-(Flat f) u) (\lambda (c: C).(clear x c)) P (\lambda (y: C).(\lambda (H0: 
-(clear x y)).(clear_ind (\lambda (_: C).(\lambda (c0: C).((eq C c0 (CHead e 
-(Flat f) u)) \to P))) (\lambda (b: B).(\lambda (e0: C).(\lambda (u0: 
-T).(\lambda (H1: (eq C (CHead e0 (Bind b) u0) (CHead e (Flat f) u))).(let H2 
-\def (eq_ind C (CHead e0 (Bind b) u0) (\lambda (ee: C).(match ee in C return 
-(\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) 
-\Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _) 
-\Rightarrow True | (Flat _) \Rightarrow False])])) I (CHead e (Flat f) u) H1) 
-in (False_ind P H2)))))) (\lambda (e0: C).(\lambda (c: C).(\lambda (H1: 
-(clear e0 c)).(\lambda (H2: (((eq C c (CHead e (Flat f) u)) \to P))).(\lambda 
-(_: F).(\lambda (_: T).(\lambda (H3: (eq C c (CHead e (Flat f) u))).(let H4 
-\def (eq_ind C c (\lambda (c0: C).((eq C c0 (CHead e (Flat f) u)) \to P)) H2 
-(CHead e (Flat f) u) H3) in (let H5 \def (eq_ind C c (\lambda (c0: C).(clear 
-e0 c0)) H1 (CHead e (Flat f) u) H3) in (H4 (refl_equal C (CHead e (Flat f) 
-u)))))))))))) x y H0))) H)))))).
+(Flat f) u) (\lambda (c: C).(clear x c)) (\lambda (_: C).P) (\lambda (y: 
+C).(\lambda (H0: (clear x y)).(clear_ind (\lambda (_: C).(\lambda (c0: 
+C).((eq C c0 (CHead e (Flat f) u)) \to P))) (\lambda (b: B).(\lambda (e0: 
+C).(\lambda (u0: T).(\lambda (H1: (eq C (CHead e0 (Bind b) u0) (CHead e (Flat 
+f) u))).(let H2 \def (eq_ind C (CHead e0 (Bind b) u0) (\lambda (ee: C).(match 
+ee in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | 
+(CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with 
+[(Bind _) \Rightarrow True | (Flat _) \Rightarrow False])])) I (CHead e (Flat 
+f) u) H1) in (False_ind P H2)))))) (\lambda (e0: C).(\lambda (c: C).(\lambda 
+(H1: (clear e0 c)).(\lambda (H2: (((eq C c (CHead e (Flat f) u)) \to 
+P))).(\lambda (_: F).(\lambda (_: T).(\lambda (H3: (eq C c (CHead e (Flat f) 
+u))).(let H4 \def (eq_ind C c (\lambda (c0: C).((eq C c0 (CHead e (Flat f) 
+u)) \to P)) H2 (CHead e (Flat f) u) H3) in (let H5 \def (eq_ind C c (\lambda 
+(c0: C).(clear e0 c0)) H1 (CHead e (Flat f) u) H3) in (H4 (refl_equal C 
+(CHead e (Flat f) u)))))))))))) x y H0))) H)))))).
 
 theorem clear_gen_all:
  \forall (c1: C).(\forall (c2: C).((clear c1 c2) \to (ex_3 B C T (\lambda (b: