we removed about 100 match-with costruction turning them into applications

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Level-1 / LambdaDelta / r / props.ma

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 709e13bb8edca1c19b4bfba0b0450a6f6d78ba13..fc8b29095132f186a18ff609a6779eee3cebb30f 100644 (file)
--- 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)))