update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / tr_id_pap.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma
index 59256fbbb2cfab01c61153504911eb5fea8a6881..2deb5bfa04b06f2a80aaeb70fa2bd8baa916627e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma
@@ -12,15 +12,15 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/relocation/tr_pap.ma".
-include "ground/relocation/tr_id.ma".
+include "ground/relocation/tr_pap_pushs.ma".
+include "ground/relocation/tr_id_pushs.ma".
 
 (* IDENTITY ELEMENT FOR TOTAL RELOCATION MAPS *******************************)
 
 (* Coonstructions with tr_pap ***********************************************)
 
-lemma tr_pap_id (p):
-      p = 𝐢@❨p❩.
-#p elim p -p //
-#p #IH <tr_id_unfold <tr_pap_succ //
+lemma tr_id_pap (p):
+      p = 𝐢＠⧣❨p❩.
+#p >(tr_pushs_id p)
+/2 width=1 by tr_pap_pushs_le/
 qed.