X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fleq%2Fasucc.ma;h=fd9e7c1d3b261aa920607b83813f23348c7bc9b8;hb=de77f79d60ee3c1d30fe03469172950b557441f3;hp=47a13f362abeb6e6e205d321454e181015c7f6c2;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/leq/asucc.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/leq/asucc.ma
index 47a13f362..fd9e7c1d3 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/leq/asucc.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/leq/asucc.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/leq/props.ma".
+include "Basic-1/leq/props.ma".
 
 theorem asucc_repl:
  \forall (g: G).(\forall (a1: A).(\forall (a2: A).((leq g a1 a2) \to (leq g 
@@ -95,6 +95,9 @@ h4) n2) k))) (aplus g (ASort (S h3) n1) k) H2) (aplus g (ASort h4 n2) k)
 (asucc g a3) (asucc g a4))).(\lambda (a5: A).(\lambda (a6: A).(\lambda (_: 
 (leq g a5 a6)).(\lambda (H3: (leq g (asucc g a5) (asucc g a6))).(leq_head g 
 a3 a4 H0 (asucc g a5) (asucc g a6) H3))))))))) a1 a2 H)))).
+(* COMMENTS
+Initial nodes: 1907
+END *)
 
 theorem asucc_inj:
  \forall (g: G).(\forall (a1: A).(\forall (a2: A).((leq g (asucc g a1) (asucc 
@@ -315,6 +318,9 @@ a4)) (AHead x0 x1) H7) in (\lambda (H10: (eq A a3 x0)).(let H11 \def
 in (let H12 \def (eq_ind_r A x0 (\lambda (a5: A).(leq g a a5)) H5 a3 H10) in 
 (leq_head g a a3 H12 a0 a4 (H0 a4 H11)))))) H8))))))) H4)))))))) a2)))))) 
 a1)).
+(* COMMENTS
+Initial nodes: 4697
+END *)
 
 theorem leq_asucc:
  \forall (g: G).(\forall (a: A).(ex A (\lambda (a0: A).(leq g a (asucc g 
@@ -331,6 +337,9 @@ A (\lambda (a0: A).(leq g (ASort n n0) (asucc g a0))) (ASort (S n) n0)
 g x))).(ex_intro A (\lambda (a2: A).(leq g (AHead a0 a1) (asucc g a2))) 
 (AHead a0 x) (leq_head g a0 a0 (leq_refl g a0) a1 (asucc g x) H2)))) H1)))))) 
 a)).
+(* COMMENTS
+Initial nodes: 221
+END *)
 
 theorem leq_ahead_asucc_false:
  \forall (g: G).(\forall (a1: A).(\forall (a2: A).((leq g (AHead a1 a2) 
@@ -388,6 +397,9 @@ _ a3) \Rightarrow a3])) (AHead a (asucc g a0)) (AHead x0 x1) H5) in (\lambda
 H4 (asucc g a0) H7) in (let H10 \def (eq_ind_r A x0 (\lambda (a3: A).(leq g 
 (AHead a a0) a3)) H3 a H8) in (leq_ahead_false_1 g a a0 H10 P))))) H6))))))) 
 H2)))))))))) a1)).
+(* COMMENTS
+Initial nodes: 927
+END *)
 
 theorem leq_asucc_false:
  \forall (g: G).(\forall (a: A).((leq g (asucc g a) a) \to (\forall (P: 
@@ -461,4 +473,7 @@ H5) in (\lambda (H8: (eq A a0 x0)).(let H9 \def (eq_ind_r A x1 (\lambda (a2:
 A).(leq g (asucc g a1) a2)) H4 a1 H7) in (let H10 \def (eq_ind_r A x0 
 (\lambda (a2: A).(leq g a0 a2)) H3 a0 H8) in (H0 H9 P))))) H6))))))) 
 H2))))))))) a)).
+(* COMMENTS
+Initial nodes: 1327
+END *)