X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLevel-1%2FLambdaDelta%2Fr%2Fprops.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLevel-1%2FLambdaDelta%2Fr%2Fprops.ma;h=fc8b29095132f186a18ff609a6779eee3cebb30f;hb=02bd27d53c28099b9fc92917cf34ccf3bc72d696;hp=709e13bb8edca1c19b4bfba0b0450a6f6d78ba13;hpb=c0a3562da676a9eb5dba565af89a3261a8c40363;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/r/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/r/props.ma
index 709e13bb8..fc8b29095 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/r/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/r/props.ma
@@ -73,10 +73,9 @@ nat).(refl_equal nat i))))))) (\lambda (f: F).(\lambda (P: Prop).(\lambda (_:
 theorem s_r:
  \forall (k: K).(\forall (i: nat).(eq nat (s k (r k i)) (S i)))
 \def
- \lambda (k: K).(match k in K return (\lambda (k0: K).(\forall (i: nat).(eq 
-nat (s k0 (r k0 i)) (S i)))) with [(Bind _) \Rightarrow (\lambda (i: 
-nat).(refl_equal nat (S i))) | (Flat _) \Rightarrow (\lambda (i: 
-nat).(refl_equal nat (S i)))]).
+ \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(eq nat (s k0 (r k0 
+i)) (S i)))) (\lambda (_: B).(\lambda (i: nat).(refl_equal nat (S i)))) 
+(\lambda (_: F).(\lambda (i: nat).(refl_equal nat (S i)))) k).
 
 theorem r_arith0:
  \forall (k: K).(\forall (i: nat).(eq nat (minus (r k (S i)) (S O)) (r k i)))