X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_1%2Fplist%2Fprops.ma;h=f80d0b0e9de06fbbd5fb2ddb2c45eea45dad9511;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=18cf0589eedf4ec26a1703ac2d713b90f4d978b8;hpb=9c954a9a843ebb1bf189536df4e14f77132ed1cf;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_1/plist/props.ma b/matita/matita/contribs/lambdadelta/ground_1/plist/props.ma
index 18cf0589e..f80d0b0e9 100644
--- a/matita/matita/contribs/lambdadelta/ground_1/plist/props.ma
+++ b/matita/matita/contribs/lambdadelta/ground_1/plist/props.ma
@@ -16,27 +16,16 @@
 
 include "ground_1/plist/defs.ma".
 
-theorem papp_ss:
+lemma papp_ss:
  \forall (is1: PList).(\forall (is2: PList).(eq PList (papp (Ss is1) (Ss 
 is2)) (Ss (papp is1 is2))))
 \def
- \lambda (is1: PList).(let TMP_885 \def (\lambda (p: PList).(\forall (is2: 
-PList).(let TMP_883 \def (Ss p) in (let TMP_882 \def (Ss is2) in (let TMP_884 
-\def (papp TMP_883 TMP_882) in (let TMP_880 \def (papp p is2) in (let TMP_881 
-\def (Ss TMP_880) in (eq PList TMP_884 TMP_881)))))))) in (let TMP_879 \def 
-(\lambda (is2: PList).(let TMP_878 \def (Ss is2) in (refl_equal PList 
-TMP_878))) in (let TMP_877 \def (\lambda (n: nat).(\lambda (n0: nat).(\lambda 
-(p: PList).(\lambda (H: ((\forall (is2: PList).(eq PList (papp (Ss p) (Ss 
-is2)) (Ss (papp p is2)))))).(\lambda (is2: PList).(let TMP_875 \def (papp p 
-is2) in (let TMP_876 \def (Ss TMP_875) in (let TMP_874 \def (\lambda (p0: 
-PList).(let TMP_872 \def (S n0) in (let TMP_873 \def (PCons n TMP_872 p0) in 
-(let TMP_870 \def (S n0) in (let TMP_868 \def (papp p is2) in (let TMP_869 
-\def (Ss TMP_868) in (let TMP_871 \def (PCons n TMP_870 TMP_869) in (eq PList 
-TMP_873 TMP_871)))))))) in (let TMP_865 \def (S n0) in (let TMP_863 \def 
-(papp p is2) in (let TMP_864 \def (Ss TMP_863) in (let TMP_866 \def (PCons n 
-TMP_865 TMP_864) in (let TMP_867 \def (refl_equal PList TMP_866) in (let 
-TMP_861 \def (Ss p) in (let TMP_860 \def (Ss is2) in (let TMP_862 \def (papp 
-TMP_861 TMP_860) in (let TMP_859 \def (H is2) in (eq_ind_r PList TMP_876 
-TMP_874 TMP_867 TMP_862 TMP_859)))))))))))))))))) in (PList_ind TMP_885 
-TMP_879 TMP_877 is1)))).
+ \lambda (is1: PList).(PList_ind (\lambda (p: PList).(\forall (is2: 
+PList).(eq PList (papp (Ss p) (Ss is2)) (Ss (papp p is2))))) (\lambda (is2: 
+PList).(refl_equal PList (Ss is2))) (\lambda (n: nat).(\lambda (n0: 
+nat).(\lambda (p: PList).(\lambda (H: ((\forall (is2: PList).(eq PList (papp 
+(Ss p) (Ss is2)) (Ss (papp p is2)))))).(\lambda (is2: PList).(eq_ind_r PList 
+(Ss (papp p is2)) (\lambda (p0: PList).(eq PList (PCons n (S n0) p0) (PCons n 
+(S n0) (Ss (papp p is2))))) (refl_equal PList (PCons n (S n0) (Ss (papp p 
+is2)))) (papp (Ss p) (Ss is2)) (H is2))))))) is1).