X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fi_dynamic%2Fntas_nta.ma;h=7374d2df420897f58a96962a2874aa50d864b45c;hp=c9ae6d1ebf90b6c5efb52825d0a2b4086fd1aacf;hb=f308429a0fde273605a2330efc63268b4ac36c99;hpb=87f57ddc367303c33e19c83cd8989cd561f3185b

diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_nta.ma b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_nta.ma
index c9ae6d1eb..7374d2df4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_nta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_nta.ma
@@ -25,8 +25,8 @@ definition ntas: sh → lenv → relation term ≝
 (* Basic eliminators ********************************************************)
 
 axiom ntas_ind_dx: ∀h,L,T2. ∀R:predicate term. R T2 →
-                   (∀T1,T. ⦃h, L⦄ ⊢ T1 : T → ⦃h, L⦄ ⊢ T :* T2 → R T → R T1) →
-                   ∀T1. ⦃h, L⦄ ⊢ T1 :* T2 → R T1.
+                   (∀T1,T. ⦃h,L⦄ ⊢ T1 : T → ⦃h,L⦄ ⊢ T :* T2 → R T → R T1) →
+                   ∀T1. ⦃h,L⦄ ⊢ T1 :* T2 → R T1.
 (*
 #h #L #T2 #R #HT2 #IHT2 #T1 #HT12
 @(star_ind_dx … HT2 IHT2 … HT12) //
@@ -35,10 +35,10 @@ qed-.
 (* Basic properties *********************************************************)
 
 lemma ntas_strap1: ∀h,L,T1,T,T2.
-                   ⦃h, L⦄ ⊢ T1 :* T → ⦃h, L⦄  ⊢ T : T2 → ⦃h, L⦄  ⊢ T1 :* T2.
+                   ⦃h,L⦄ ⊢ T1 :* T → ⦃h,L⦄  ⊢ T : T2 → ⦃h,L⦄  ⊢ T1 :* T2.
 /2 width=3/ qed.
 
 lemma ntas_strap2: ∀h,L,T1,T,T2.
-                   ⦃h, L⦄  ⊢ T1 : T → ⦃h, L⦄ ⊢ T :* T2 → ⦃h, L⦄ ⊢ T1 :* T2.
+                   ⦃h,L⦄  ⊢ T1 : T → ⦃h,L⦄ ⊢ T :* T2 → ⦃h,L⦄ ⊢ T1 :* T2.
 /2 width=3/ qed.
 *)