partial update in static_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / syntax / sh_nexts.ma

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 143e2dbb89a8f5154c6359910e8e52d9bec3e488..f9c69e429aa1e0225a1b2ba8bfadaa5f2763a6ed 100644 (file)
--- 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.