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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubt/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubt/fwd.ma
index 06c651505..63a3eca47 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubt/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csubt/fwd.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/csubt/defs.ma".
+include "Basic-1/csubt/defs.ma".
 
 theorem csubt_gen_abbr:
  \forall (g: G).(\forall (e1: C).(\forall (c2: C).(\forall (v: T).((csubt g 
@@ -82,6 +82,9 @@ ee in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False |
 _) \Rightarrow False])])) I (CHead e1 (Bind Abbr) v) H5) in (False_ind (ex2 C 
 (\lambda (e2: C).(eq C (CHead c3 (Bind Abbr) u) (CHead e2 (Bind Abbr) v))) 
 (\lambda (e2: C).(csubt g e1 e2))) H6))))))))))) y c2 H0))) H))))).
+(* COMMENTS
+Initial nodes: 1111
+END *)
 
 theorem csubt_gen_abst:
  \forall (g: G).(\forall (e1: C).(\forall (c2: C).(\forall (v1: T).((csubt g 
@@ -209,6 +212,9 @@ Abbr) u) (CHead e2 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_: T).(csubt
 g e1 e2))) (\lambda (_: C).(\lambda (v2: T).(ty3 g e1 v2 v1))) (\lambda (e2: 
 C).(\lambda (v2: T).(ty3 g e2 v2 v1))) c3 u (refl_equal C (CHead c3 (Bind 
 Abbr) u)) H13 H11 H9))))))))) H6))))))))))) y c2 H0))) H))))).
+(* COMMENTS
+Initial nodes: 2362
+END *)
 
 theorem csubt_gen_flat:
  \forall (g: G).(\forall (e1: C).(\forall (c2: C).(\forall (v: T).(\forall 
@@ -272,6 +278,9 @@ t)).(\lambda (_: (ty3 g c3 u t)).(\lambda (H5: (eq C (CHead c1 (Bind Abst) t)
 False])])) I (CHead e1 (Flat f) v) H5) in (False_ind (ex2 C (\lambda (e2: 
 C).(eq C (CHead c3 (Bind Abbr) u) (CHead e2 (Flat f) v))) (\lambda (e2: 
 C).(csubt g e1 e2))) H6))))))))))) y c2 H0))) H)))))).
+(* COMMENTS
+Initial nodes: 1103
+END *)
 
 theorem csubt_gen_bind:
  \forall (g: G).(\forall (b1: B).(\forall (e1: C).(\forall (c2: C).(\forall 
@@ -383,4 +392,7 @@ B).(\lambda (e2: C).(\lambda (v2: T).(eq C (CHead c3 (Bind Abbr) u) (CHead e2
 (Bind b2) v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csubt g 
 e1 e2)))) Abbr c3 u (refl_equal C (CHead c3 (Bind Abbr) u)) H15)))))))))) 
 H7)) H6))))))))))) y c2 H0))) H)))))).
+(* COMMENTS
+Initial nodes: 1899
+END *)