fixed some regressions

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / LambdaDelta-1 / ex1 / props.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/props.ma
index e809b11bfa9a37490e6b1bda5644c853bdbc527d..9c94c211177c8bcaec4d6b157ba8e6b1f3d24801 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/props.ma
@@ -14,19 +14,19 @@
 
 (* This file was automatically generated: do not edit *********************)
 
 
 (* This file was automatically generated: do not edit *********************)
 

-include "ex1/defs.ma".
+include "LambdaDelta-1/ex1/defs.ma".

 
 

-include "ty3/fwd.ma".
+include "LambdaDelta-1/ty3/fwd.ma".

 
 

-include "pc3/fwd.ma".
+include "LambdaDelta-1/pc3/fwd.ma".

 
 

-include "nf2/pr3.ma".
+include "LambdaDelta-1/nf2/pr3.ma".

 
 

-include "nf2/props.ma".
+include "LambdaDelta-1/nf2/props.ma".

 
 

-include "arity/defs.ma".
+include "LambdaDelta-1/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 
 
 theorem ex1__leq_sort_SS:
  \forall (g: G).(\forall (k: nat).(\forall (n: nat).(leq g (ASort k n) (asucc 


@@ -460,7 +460,7 @@ x10 t x12)) H33 (TSort O) H35) in (let H38 \def (eq_ind T x11 (\lambda (t:
 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) 
 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 
 (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