From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 7 Aug 2022 17:37:11 +0000 (+0200)
Subject: update in ground
X-Git-Tag: make_still_working~45^2
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=afb5d82d388986bbeb17a4f114aebbaafc948f93

update in ground

+ additions to nap and xap
---

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma
index ac32304ed..a5ab2dcb7 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma
@@ -1,5 +1,6 @@
 include "ground/relocation/tr_uni_pap.ma".
 include "ground/relocation/tr_compose_pap.ma".
+include "ground/relocation/tr_pap_eq.ma".
 include "ground/notation/functions/applysucc_2.ma".
 include "ground/arith/nat_lt.ma".
 include "ground/arith/nat_plus_rplus.ma".
@@ -53,3 +54,10 @@ lemma tr_nap_pushs_lt (f) (n) (m):
 <tr_nap_unfold <tr_pap_pushs_le
 /2 width=1 by nlt_npsucc_bi/
 qed-.
+
+theorem tr_nap_eq_repl (i):
+        stream_eq_repl … (λf1,f2. f1@↑❨i❩ = f2@↑❨i❩).
+#i #f1 #f2 #Hf
+<tr_nap_unfold <tr_nap_unfold
+/3 width=1 by tr_pap_eq_repl, eq_f/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma
index a9096f7e4..073ffed7f 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma
@@ -1,6 +1,7 @@
 
 (**) (* reverse include *)
 include "ground/arith/nat_rplus_pplus.ma".
+include "ground/relocation/tr_pn_eq.ma".
 include "ground/relocation/tr_compose_pn.ma".
 include "ground/relocation/nap.ma".
 include "ground/notation/functions/apply_2.ma".
@@ -70,3 +71,10 @@ lemma tr_xap_plus (n1) (n2) (f):
 <nrplus_inj_sn <nrplus_inj_dx
 >tr_pap_plus //
 qed.
+
+theorem tr_xap_eq_repl (i):
+        stream_eq_repl … (λf1,f2. f1＠❨i❩ = f2＠❨i❩).
+#i #f1 #f2 #Hf
+<tr_xap_unfold <tr_xap_unfold
+/3 width=1 by tr_push_eq_repl, tr_nap_eq_repl/
+qed.