X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda%2Fsn.ma;h=a9fbff3700afc50ae67e78db40b3e966bf60ebfd;hb=100184e7920cc3c70b50b694a17fa40ecde45e77;hp=c30cfecc7619d6714779ca165ffd96d59562390f;hpb=87d894fbd1d1c6ae4f9a8421ffa39af838b72e9f;p=helm.git

diff --git a/matita/matita/lib/lambda/sn.ma b/matita/matita/lib/lambda/sn.ma
index c30cfecc7..a9fbff370 100644
--- a/matita/matita/lib/lambda/sn.ma
+++ b/matita/matita/lib/lambda/sn.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda/ext.ma".
+include "lambda/ext_lambda.ma".
 
 (* STRONGLY NORMALIZING TERMS *************************************************)
 
@@ -34,12 +34,21 @@ definition SAT1 ≝ λ(P:?->Prop). ∀i,l. SNl l → P (Appl (Rel i) l).
 definition SAT2 ≝ λ(P:?→Prop). ∀N,L,M,l. SN N → SN L → 
                   P (Appl M[0:=L] l) → P (Appl (Lambda N M) (L::l)).
 
-theorem SAT0_sort: ∀P,n. SAT0 P → P (Sort n).
-#P #n #H @(H n (nil ?) …) //
+definition SAT3 ≝ λ(P:?→Prop). ∀M,N,l. P (Appl (D (App M N)) l) → 
+                               P (Appl (D M) (N::l)).
+
+definition SAT4 ≝ λ(P:?→Prop). ∀M. P M → P (D M).
+
+lemma SAT0_sort: ∀P,n. SAT0 P → P (Sort n).
+#P #n #HP @(HP n (nil ?) …) //
+qed.
+
+lemma SAT1_rel: ∀P,i. SAT1 P → P (Rel i).
+#P #i #HP @(HP i (nil ?) …) //
 qed.
 
-theorem SAT1_rel: ∀P,i. SAT1 P → P (Rel i).
-#P #i #H @(H i (nil ?) …) //
+lemma SAT3_1: ∀P,M,N. SAT3 P → P (D (App M N)) → P (App (D M) N).
+#P #M #N #HP #H @(HP … ([])) @H
 qed.
 
 (* axiomatization *************************************************************)
@@ -50,10 +59,12 @@ axiom sn_rel: SAT1 SN.
 
 axiom sn_beta: SAT2 SN.
 
+axiom sn_dapp: SAT3 SN.
+
+axiom sn_dummy: SAT4 SN.
+
 axiom sn_lambda: ∀N,M. SN N → SN M → SN (Lambda N M).
 
 axiom sn_prod: ∀N,M. SN N → SN M → SN (Prod N M).
 
-axiom sn_dummy: ∀M. SN M → SN (D M).
-
 axiom sn_inv_app_1: ∀M,N. SN (App M N) → SN M.