(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/llt/props".
+include "LambdaDelta-1/llt/defs.ma".
-include "llt/defs.ma".
-
-include "leq/defs.ma".
+include "LambdaDelta-1/leq/defs.ma".
theorem lweight_repl:
\forall (g: G).(\forall (a1: A).(\forall (a2: A).((leq g a1 a2) \to (eq nat
theorem llt_head_sx:
\forall (a1: A).(\forall (a2: A).(llt a1 (AHead a1 a2)))
\def
- \lambda (a1: A).(\lambda (a2: A).(le_S_n (S (lweight a1)) (S (plus (lweight
-a1) (lweight a2))) (le_n_S (S (lweight a1)) (S (plus (lweight a1) (lweight
-a2))) (le_n_S (lweight a1) (plus (lweight a1) (lweight a2)) (le_plus_l
-(lweight a1) (lweight a2)))))).
+ \lambda (a1: A).(\lambda (a2: A).(le_n_S (lweight a1) (plus (lweight a1)
+(lweight a2)) (le_plus_l (lweight a1) (lweight a2)))).
theorem llt_head_dx:
\forall (a1: A).(\forall (a2: A).(llt a2 (AHead a1 a2)))
\def
- \lambda (a1: A).(\lambda (a2: A).(le_S_n (S (lweight a2)) (S (plus (lweight
-a1) (lweight a2))) (le_n_S (S (lweight a2)) (S (plus (lweight a1) (lweight
-a2))) (le_n_S (lweight a2) (plus (lweight a1) (lweight a2)) (le_plus_r
-(lweight a1) (lweight a2)))))).
+ \lambda (a1: A).(\lambda (a2: A).(le_n_S (lweight a2) (plus (lweight a1)
+(lweight a2)) (le_plus_r (lweight a1) (lweight a2)))).
theorem llt_wf__q_ind:
\forall (P: ((A \to Prop))).(((\forall (n: nat).((\lambda (P0: ((A \to