some restyling ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / i_dynamic / ntas_nta.ma

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 c9ae6d1ebf90b6c5efb52825d0a2b4086fd1aacf..7374d2df420897f58a96962a2874aa50d864b45c 100644 (file)
--- 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.
 *)