X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fleq%2Fasucc.ma;h=25f9dfd074c944c466a5f7639c86be2eb7a4556f;hb=fdda444a05fe4c68c925cd94e4e3a38c93d0c35f;hp=c996451b46b4f9fed0e2337a5f2b455fe27e35f5;hpb=9376f52b7f5890d924ae7d93bcae2af9e516126d;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/asucc.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/asucc.ma
index c996451b4..25f9dfd07 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/asucc.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/asucc.ma
@@ -612,10 +612,10 @@ return (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a4 | (AHead a7 _)
 ((leq g a2 a6) \to P)))) (\lambda (H12: (eq A a6 (asucc g a0))).(eq_ind A 
 (asucc g a0) (\lambda (a7: A).((leq g (AHead a a0) a) \to ((leq g a2 a7) \to 
 P))) (\lambda (H13: (leq g (AHead a a0) a)).(\lambda (_: (leq g a2 (asucc g 
-a0))).(leq_ahead_false g a a0 H13 P))) a6 (sym_eq A a6 (asucc g a0) H12))) a4 
-(sym_eq A a4 a H11))) H10))) a5 (sym_eq A a5 a2 H8))) a3 (sym_eq A a3 (AHead 
-a a0) H7))) H6)) H5 H2 H3)))]) in (H2 (refl_equal A (AHead (AHead a a0) a2)) 
-(refl_equal A (AHead a (asucc g a0)))))))))))) a1)).
+a0))).(leq_ahead_false_1 g a a0 H13 P))) a6 (sym_eq A a6 (asucc g a0) H12))) 
+a4 (sym_eq A a4 a H11))) H10))) a5 (sym_eq A a5 a2 H8))) a3 (sym_eq A a3 
+(AHead a a0) H7))) H6)) H5 H2 H3)))]) in (H2 (refl_equal A (AHead (AHead a 
+a0) a2)) (refl_equal A (AHead a (asucc g a0)))))))))))) a1)).
 
 theorem leq_asucc_false:
  \forall (g: G).(\forall (a: A).((leq g (asucc g a) a) \to (\forall (P: