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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csuba/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csuba/fwd.ma
index 34d188209..a618761fe 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csuba/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/csuba/fwd.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/csuba/defs.ma".
+include "Basic-1/csuba/defs.ma".
 
 theorem csuba_gen_abbr:
  \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u: T).((csuba g 
@@ -83,6 +83,9 @@ B).Prop) with [Abbr \Rightarrow False | Abst \Rightarrow True | Void
 u) H5) in (False_ind (ex2 C (\lambda (d2: C).(eq C (CHead c2 (Bind Abbr) u0) 
 (CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(csuba g d1 d2))) H6)))))))))))) 
 y c H0))) H))))).
+(* COMMENTS
+Initial nodes: 1117
+END *)
 
 theorem csuba_gen_void:
  \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u1: T).((csuba g 
@@ -169,6 +172,9 @@ True | Void \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead d1
 C).(\lambda (u2: T).(eq C (CHead c2 (Bind Abbr) u) (CHead d2 (Bind b) u2))))) 
 (\lambda (_: B).(\lambda (d2: C).(\lambda (_: T).(csuba g d1 d2))))) 
 H6)))))))))))) y c H0))) H))))).
+(* COMMENTS
+Initial nodes: 1418
+END *)
 
 theorem csuba_gen_abst:
  \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u1: T).((csuba g 
@@ -314,6 +320,9 @@ u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
 a0))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0: A).(arity g d2 u2 
 a0)))) c2 u a (refl_equal C (CHead c2 (Bind Abbr) u)) H12 H10 H4)))))))) 
 H6)))))))))))) y c H0))) H))))).
+(* COMMENTS
+Initial nodes: 2550
+END *)
 
 theorem csuba_gen_flat:
  \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u1: T).(\forall 
@@ -385,6 +394,9 @@ _) \Rightarrow False])])) I (CHead d1 (Flat f) u1) H5) in (False_ind (ex2_2 C
 T (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c2 (Bind Abbr) u) (CHead d2 
 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d1 d2)))) 
 H6)))))))))))) y c H0))) H)))))).
+(* COMMENTS
+Initial nodes: 1183
+END *)
 
 theorem csuba_gen_bind:
  \forall (g: G).(\forall (b1: B).(\forall (e1: C).(\forall (c2: C).(\forall 
@@ -496,6 +508,9 @@ 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).(csuba g 
 e1 e2)))) Abbr c3 u (refl_equal C (CHead c3 (Bind Abbr) u)) H14))))))))) H7)) 
 H6)))))))))))) y c2 H0))) H)))))).
+(* COMMENTS
+Initial nodes: 1889
+END *)
 
 theorem csuba_gen_abst_rev:
  \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u: T).((csuba g c 
@@ -605,6 +620,9 @@ c1 (Bind Abst) t) (CHead d2 (Bind Abst) u))) (\lambda (d2: C).(csuba g d2
 d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c1 (Bind 
 Abst) t) (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba 
 g d2 d1))))) H6)))))))))))) c y H0))) H))))).
+(* COMMENTS
+Initial nodes: 1980
+END *)
 
 theorem csuba_gen_void_rev:
  \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u: T).((csuba g c 
@@ -683,6 +701,9 @@ False | Void \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead
 d1 (Bind Void) u) H5) in (False_ind (ex2 C (\lambda (d2: C).(eq C (CHead c1 
 (Bind Abst) t) (CHead d2 (Bind Void) u))) (\lambda (d2: C).(csuba g d2 d1))) 
 H6)))))))))))) c y H0))) H))))).
+(* COMMENTS
+Initial nodes: 1326
+END *)
 
 theorem csuba_gen_abbr_rev:
  \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u1: T).((csuba g c 
@@ -871,6 +892,9 @@ d2 d1)))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a0: A).(arity g d2 u2
 (asucc g a0))))) (\lambda (_: C).(\lambda (_: T).(\lambda (a0: A).(arity g d1 
 u1 a0)))) c1 t a (refl_equal C (CHead c1 (Bind Abst) t)) H12 H3 H10)))))))) 
 H6)))))))))))) c y H0))) H))))).
+(* COMMENTS
+Initial nodes: 3459
+END *)
 
 theorem csuba_gen_flat_rev:
  \forall (g: G).(\forall (d1: C).(\forall (c: C).(\forall (u1: T).(\forall 
@@ -942,6 +966,9 @@ _) \Rightarrow False])])) I (CHead d1 (Flat f) u1) H5) in (False_ind (ex2_2 C
 T (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c1 (Bind Abst) t) (CHead d2 
 (Flat f) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d1)))) 
 H6)))))))))))) c y H0))) H)))))).
+(* COMMENTS
+Initial nodes: 1183
+END *)
 
 theorem csuba_gen_bind_rev:
  \forall (g: G).(\forall (b1: B).(\forall (e1: C).(\forall (c2: C).(\forall 
@@ -1050,4 +1077,7 @@ C).(\lambda (v2: T).(eq C (CHead c1 (Bind Abst) t) (CHead e2 (Bind b2)
 v2))))) (\lambda (_: B).(\lambda (e2: C).(\lambda (_: T).(csuba g e2 e1)))) 
 Abst c1 t (refl_equal C (CHead c1 (Bind Abst) t)) H14))))))))) H7)) 
 H6)))))))))))) c2 y H0))) H)))))).
+(* COMMENTS
+Initial nodes: 1831
+END *)