From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 27 Apr 2022 17:34:39 +0000 (+0200)
Subject: update in ground
X-Git-Tag: make_still_working~76^2~4
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=d54b569f6bf95945a851455c0a13b08c51ddce60

update in ground

+ some addittions and corrections
---

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma
index 742c6b257..660d4147a 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma
@@ -41,6 +41,9 @@ lemma npsucc_zero: (𝟏) = ↑𝟎.
 lemma npsucc_inj (p): (↑p) = ↑(ninj p).
 // qed.
 
+lemma nsucc_unfold (n): ninj (↑n) = ↑n.
+// qed-.
+
 lemma nsucc_zero: ninj (𝟏) = ↑𝟎.
 // qed.
 
diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
index 322235e7a..00faad83d 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
@@ -40,7 +40,7 @@ lemma list_append_rcons_sn (A):
 // qed.
 
 lemma list_append_rcons_dx (A):
-      ∀l1,l2,a. l1 ⨁ l2 ⨭ a = l1 ⨁{A} (l2 ⨭ a).
+      ∀l1,l2,a. (l1 ⨁ l2) ⨭ a = l1 ⨁{A} (l2 ⨭ a).
 // qed.
 
 (* Basic inversions *********************************************************)
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma
index 54cf97875..d278582f2 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma
@@ -29,6 +29,12 @@ qed.
 
 (* Constructions with tr_compose and tr_tls *********************************)
 
+lemma tr_tls_compose_uni_sn (f) (n) (p:pnat):
+      ⇂*[p]f ≗ ⇂*[p](𝐮❨n❩∘f).
+#f #n #p elim p -p //
+#p #IH /2 width=1 by stream_tl_eq_repl/
+qed.
+
 lemma tr_tl_compose_uni_dx (f) (n):
       ⇂*[↑n]f ≗ ⇂(f∘𝐮❨n❩).
 // qed.