X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fsyntax%2Fsh_nexts.ma;h=f9c69e429aa1e0225a1b2ba8bfadaa5f2763a6ed;hp=143e2dbb89a8f5154c6359910e8e52d9bec3e488;hb=8fe4dc148d50a0352313633bea61441bc817afbf;hpb=cab35e3d6c09d266c1372b5cc9a0045578bae79b

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/sh_nexts.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/sh_nexts.ma
index 143e2dbb8..f9c69e429 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/sh_nexts.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/sh_nexts.ma
@@ -26,21 +26,28 @@ interpretation
 
 (* Basic constructions *)
 
-lemma sh_nexts_zero (h): ∀s. s = ⇡*[h,𝟎]s.
+lemma sh_nexts_zero (h):
+      ∀s. s = ⇡*[h,𝟎]s.
 // qed.
 
-lemma sh_nexts_unit (h): ⇡[h] ≐ ⇡*[h,𝟏].
+lemma sh_nexts_unit (h):
+      ∀s. ⇡[h]s = ⇡*[h,𝟏]s.
 // qed.
 
-lemma sh_nexts_succ (h) (n): ⇡[h] ∘ (⇡*[h,n]) ≐ ⇡*[h,↑n].
-/2 width=1 by niter_succ/ qed.
+lemma sh_nexts_succ (h) (n):
+      ∀s. ⇡[h](⇡*[h,n]s) = ⇡*[h,↑n]s.
+#h #n #s @(niter_succ … (⇡[h]))
+qed.
 
 (* Advanced constructions ****************************)
 
-lemma sh_nexts_swap (h) (n): ⇡[h] ∘ (⇡*[h,n]) ≐ ⇡*[h,n] ∘ ⇡[h].
-/2 width=1 by niter_appl/ qed.
+lemma sh_nexts_swap (h) (n):
+      ∀s. ⇡[h](⇡*[h,n]s) = ⇡*[h,n](⇡[h]s).
+#h #n #s @(niter_appl … (⇡[h]))
+qed.
 
 (* Helper constructions *****************************************************)
 
-lemma sh_nexts_succ_next (h) (n): ⇡*[h,n] ∘ (⇡[h]) ≐ ⇡*[h,↑n].
+lemma sh_nexts_succ_next (h) (n):
+      ∀s. ⇡*[h,n](⇡[h]s) = ⇡*[h,↑n]s.
 // qed.