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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/asucc/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/asucc/fwd.ma
index f8fae3129..61fcb5799 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/asucc/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/asucc/fwd.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/asucc/defs.ma".
+include "Basic-1/asucc/defs.ma".
 
 theorem asucc_gen_sort:
  \forall (g: G).(\forall (h: nat).(\forall (n: nat).(\forall (a: A).((eq A 
@@ -39,6 +39,9 @@ n0)))))))).(\lambda (H1: (eq A (ASort h n) (asucc g (AHead a0 a1)))).(let H2
 False])) I (asucc g (AHead a0 a1)) H1) in (False_ind (ex_2 nat nat (\lambda 
 (h0: nat).(\lambda (n0: nat).(eq A (AHead a0 a1) (ASort h0 n0))))) H2))))))) 
 a)))).
+(* COMMENTS
+Initial nodes: 317
+END *)
 
 theorem asucc_gen_head:
  \forall (g: G).(\forall (a1: A).(\forall (a2: A).(\forall (a: A).((eq A 
@@ -90,4 +93,7 @@ a1 a4) (asucc g a3)) \to (ex2 A (\lambda (a5: A).(eq A a3 (AHead a1 a5)))
 a1 a3) (AHead a1 a4))) (\lambda (a4: A).(eq A (asucc g a3) (asucc g a4))) a3 
 (refl_equal A (AHead a1 a3)) (refl_equal A (asucc g a3))) a2 H3))) a0 H4)))) 
 H2))))))) a)))).
+(* COMMENTS
+Initial nodes: 957
+END *)