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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/iso/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/iso/fwd.ma
index e2fb05409..761e982f7 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/iso/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/iso/fwd.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/iso/defs.ma".
+include "Basic-1/iso/defs.ma".
 
-include "LambdaDelta-1/tlist/defs.ma".
+include "Basic-1/tlist/defs.ma".
 
 theorem iso_gen_sort:
  \forall (u2: T).(\forall (n1: nat).((iso (TSort n1) u2) \to (ex nat (\lambda 
@@ -43,6 +43,9 @@ K).(\lambda (H1: (eq T (THead k v1 t1) (TSort n1))).(let H2 \def (eq_ind T
 with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ 
 _) \Rightarrow True])) I (TSort n1) H1) in (False_ind (ex nat (\lambda (n2: 
 nat).(eq T (THead k v2 t2) (TSort n2)))) H2)))))))) y u2 H0))) H))).
+(* COMMENTS
+Initial nodes: 321
+END *)
 
 theorem iso_gen_lref:
  \forall (u2: T).(\forall (n1: nat).((iso (TLRef n1) u2) \to (ex nat (\lambda 
@@ -69,6 +72,9 @@ K).(\lambda (H1: (eq T (THead k v1 t1) (TLRef n1))).(let H2 \def (eq_ind T
 with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ 
 _) \Rightarrow True])) I (TLRef n1) H1) in (False_ind (ex nat (\lambda (n2: 
 nat).(eq T (THead k v2 t2) (TLRef n2)))) H2)))))))) y u2 H0))) H))).
+(* COMMENTS
+Initial nodes: 321
+END *)
 
 theorem iso_gen_head:
  \forall (k: K).(\forall (v1: T).(\forall (t1: T).(\forall (u2: T).((iso 
@@ -108,6 +114,9 @@ v0 v1)).(\lambda (H6: (eq K k0 k)).(eq_ind_r K k (\lambda (k1: K).(ex_2 T T
 (ex_2_intro T T (\lambda (v3: T).(\lambda (t3: T).(eq T (THead k v2 t2) 
 (THead k v3 t3)))) v2 t2 (refl_equal T (THead k v2 t2))) k0 H6)))) H3)) 
 H2)))))))) y u2 H0))) H))))).
+(* COMMENTS
+Initial nodes: 545
+END *)
 
 theorem iso_flats_lref_bind_false:
  \forall (f: F).(\forall (b: B).(\forall (i: nat).(\forall (v: T).(\forall 
@@ -138,6 +147,9 @@ ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False |
 (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow 
 False])])) I (THead (Flat f) x0 x1) H2) in (False_ind P H3))))) H1)))))))) 
 vs)))))).
+(* COMMENTS
+Initial nodes: 391
+END *)
 
 theorem iso_flats_flat_bind_false:
  \forall (f1: F).(\forall (f2: F).(\forall (b: B).(\forall (v: T).(\forall 
@@ -173,4 +185,7 @@ T).(\lambda (H2: (eq T (THead (Bind b) v t) (THead (Flat f1) x0 x1))).(let H3
 (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow 
 False])])) I (THead (Flat f1) x0 x1) H2) in (False_ind P H3))))) H1)))))))) 
 vs)))))))).
+(* COMMENTS
+Initial nodes: 461
+END *)