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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/iso/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/iso/props.ma
index 961bf3b2a..af521d073 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/iso/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/iso/props.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/iso/fwd.ma".
+include "Basic-1/iso/fwd.ma".
 
 theorem iso_refl:
  \forall (t: T).(iso t t)
@@ -23,6 +23,9 @@ theorem iso_refl:
 nat).(iso_sort n n)) (\lambda (n: nat).(iso_lref n n)) (\lambda (k: 
 K).(\lambda (t0: T).(\lambda (_: (iso t0 t0)).(\lambda (t1: T).(\lambda (_: 
 (iso t1 t1)).(iso_head t0 t0 t1 t1 k)))))) t).
+(* COMMENTS
+Initial nodes: 59
+END *)
 
 theorem iso_trans:
  \forall (t1: T).(\forall (t2: T).((iso t1 t2) \to (\forall (t3: T).((iso t2 
@@ -47,4 +50,7 @@ t3) \to (iso t1 t3)))))
 (\lambda (x0: T).(\lambda (x1: T).(\lambda (H2: (eq T t5 (THead k x0 
 x1))).(eq_ind_r T (THead k x0 x1) (\lambda (t: T).(iso (THead k v1 t3) t)) 
 (iso_head v1 x0 t3 x1 k) t5 H2)))) H1)))))))))) t1 t2 H))).
+(* COMMENTS
+Initial nodes: 351
+END *)