(* This file was automatically generated: do not edit *********************)
-include "lift/fwd.ma".
+include "LambdaDelta-1/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
\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