cicInspect: now we can choose not to count the Cic.Implicit constructors

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / LambdaDelta-1 / lift / tlt.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/tlt.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/tlt.ma
index 0e041d02d883d27e7b2a48a323ab5dc281ebd420..4e088a12270bd030cc74ed1d1e7b8b7bca045471 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/tlt.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/tlt.ma
@@ -14,11 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift/tlt".
+include "LambdaDelta-1/lift/fwd.ma".
 
-include "lift/fwd.ma".
-
-include "tlt/props.ma".
+include "LambdaDelta-1/tlt/props.ma".
 
 theorem lift_weight_map:
  \forall (t: T).(\forall (h: nat).(\forall (d: nat).(\forall (f: ((nat \to 
@@ -271,17 +269,9 @@ O t))))))
 \def
  \lambda (w: nat).(\lambda (t: T).(\lambda (h: nat).(\lambda (f: ((nat \to 
 nat))).(lift_weight_add (plus (wadd f w O) O) t h O f (wadd f w) (\lambda (m: 
-nat).(\lambda (H: (lt m O)).(let H0 \def (match H in le return (\lambda (n: 
-nat).(\lambda (_: (le ? n)).((eq nat n O) \to (eq nat (wadd f w m) (f m))))) 
-with [le_n \Rightarrow (\lambda (H0: (eq nat (S m) O)).(let H1 \def (eq_ind 
-nat (S m) (\lambda (e: nat).(match e in nat return (\lambda (_: nat).Prop) 
-with [O \Rightarrow False | (S _) \Rightarrow True])) I O H0) in (False_ind 
-(eq nat (wadd f w m) (f m)) H1))) | (le_S m0 H0) \Rightarrow (\lambda (H1: 
-(eq nat (S m0) O)).((let H2 \def (eq_ind nat (S m0) (\lambda (e: nat).(match 
-e in nat return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) 
-\Rightarrow True])) I O H1) in (False_ind ((le (S m) m0) \to (eq nat (wadd f 
-w m) (f m))) H2)) H0))]) in (H0 (refl_equal nat O))))) (plus_n_O (wadd f w 
-O)) (\lambda (m: nat).(\lambda (_: (le O m)).(refl_equal nat (f m)))))))).
+nat).(\lambda (H: (lt m O)).(lt_x_O m H (eq nat (wadd f w m) (f m))))) 
+(plus_n_O (wadd f w O)) (\lambda (m: nat).(\lambda (_: (le O m)).(refl_equal 
+nat (f m)))))))).
 
 theorem lift_tlt_dx:
  \forall (k: K).(\forall (u: T).(\forall (t: T).(\forall (h: nat).(\forall