X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda%2Fsn.ma;h=a9fbff3700afc50ae67e78db40b3e966bf60ebfd;hb=2912d9bd61bc451c1135ca0a123cc30f203e93c9;hp=9b6478455a22a5ed18eda8b952003b7c7695f676;hpb=f3091151495bc605ce2022e55741f6420f708d8e;p=helm.git

diff --git a/matita/matita/lib/lambda/sn.ma b/matita/matita/lib/lambda/sn.ma
index 9b6478455..a9fbff370 100644
--- a/matita/matita/lib/lambda/sn.ma
+++ b/matita/matita/lib/lambda/sn.ma
@@ -34,8 +34,8 @@ 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)).
 
-definition SAT3 ≝ λ(P:?→Prop). ∀N,l1,l2. P (Appl (D (Appl N l1)) l2) → 
-                               P (Appl (D N) (l1@l2)).
+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).
 
@@ -47,8 +47,8 @@ lemma SAT1_rel: ∀P,i. SAT1 P → P (Rel i).
 #P #i #HP @(HP i (nil ?) …) //
 qed.
 
-lemma SAT3_1: ∀P,N,M. SAT3 P → P (D (App N M)) → P (App (D N) M).
-#P #N #M #HP #H @(HP … ([?]) ([])) @H
+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 *************************************************************)