X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fcsubc%2Ffwd.ma;h=fe04ddd45989b0e3f874de7f40fcecfc1f180a96;hb=de77f79d60ee3c1d30fe03469172950b557441f3;hp=2ff7d012e395a68d1e7aca1b54f4397e3b688f2b;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubc/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubc/fwd.ma
index 2ff7d012e..fe04ddd45 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubc/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubc/fwd.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/csubc/defs.ma".
+include "Basic-1/csubc/defs.ma".
 
 theorem csubc_gen_sort_l:
  \forall (g: G).(\forall (x: C).(\forall (n: nat).((csubc g (CSort n) x) \to 
@@ -50,6 +50,9 @@ w)).(\lambda (H5: (eq C (CHead c1 (Bind Abst) v) (CSort n))).(let H6 \def
 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ _ _) 
 \Rightarrow True])) I (CSort n) H5) in (False_ind (eq C (CHead c2 (Bind Abbr) 
 w) (CHead c1 (Bind Abst) v)) H6)))))))))))) y x H0))) H)))).
+(* COMMENTS
+Initial nodes: 533
+END *)
 
 theorem csubc_gen_head_l:
  \forall (g: G).(\forall (c1: C).(\forall (x: C).(\forall (v: T).(\forall (k: 
@@ -337,6 +340,9 @@ A).(csubc g c1 c3)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(sc3 g
 g a0 c3 w0)))) c2 w a (refl_equal K (Bind Abst)) (refl_equal C (CHead c2 
 (Bind Abbr) w)) H14 H12 H4)) k H9))))))))) H7)) H6)))))))))))) y x H0))) 
 H)))))).
+(* COMMENTS
+Initial nodes: 5205
+END *)
 
 theorem csubc_gen_sort_r:
  \forall (g: G).(\forall (x: C).(\forall (n: nat).((csubc g x (CSort n)) \to 
@@ -372,6 +378,9 @@ w)).(\lambda (H5: (eq C (CHead c2 (Bind Abbr) w) (CSort n))).(let H6 \def
 (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ _ _) 
 \Rightarrow True])) I (CSort n) H5) in (False_ind (eq C (CHead c1 (Bind Abst) 
 v) (CHead c2 (Bind Abbr) w)) H6)))))))))))) x y H0))) H)))).
+(* COMMENTS
+Initial nodes: 533
+END *)
 
 theorem csubc_gen_head_r:
  \forall (g: G).(\forall (c2: C).(\forall (x: C).(\forall (w: T).(\forall (k: 
@@ -658,4 +667,7 @@ g (asucc g a0) c3 v0)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0:
 A).(sc3 g a0 c2 w)))) c1 v a (refl_equal K (Bind Abbr)) (refl_equal C (CHead 
 c1 (Bind Abst) v)) H14 H3 H12)) k H9))))))))) H7)) H6)))))))))))) x y H0))) 
 H)))))).
+(* COMMENTS
+Initial nodes: 5197
+END *)