(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ex1/props".
+include "LambdaDelta-1/ex1/defs.ma".
-include "ex1/defs.ma".
+include "LambdaDelta-1/ty3/fwd.ma".
-include "ty3/fwd.ma".
+include "LambdaDelta-1/pc3/fwd.ma".
-include "pc3/fwd.ma".
+include "LambdaDelta-1/nf2/pr3.ma".
-include "nf2/pr3.ma".
+include "LambdaDelta-1/nf2/props.ma".
-include "nf2/props.ma".
+include "LambdaDelta-1/arity/defs.ma".
-include "arity/defs.ma".
-
-include "leq/props.ma".
+include "LambdaDelta-1/leq/props.ma".
theorem ex1__leq_sort_SS:
\forall (g: G).(\forall (k: nat).(\forall (n: nat).(leq g (ASort k n) (asucc
T).(pc3 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
(lift (S O) O t) x4)) H31 (TSort O) H35) in (let H39 \def (eq_ind C x10
(\lambda (c: C).(ty3 g c (TSort O) x12)) H37 (CHead (CSort O) (Bind Abst)
-(TSort O)) H36) in (and_ind (pc3 (CHead (CHead (CHead (CSort O) (Bind Abst)
+(TSort O)) H36) in (land_ind (pc3 (CHead (CHead (CHead (CSort O) (Bind Abst)
(TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O)))
x0) (\forall (b: B).(\forall (u0: T).(pc3 (CHead (CHead (CHead (CHead (CSort
O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (Bind