(* *)
(**************************************************************************)
-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 *******************************)
lemma tr_pap_id (p):
p = 𝐢@❨p❩.
-#p elim p -p //
-#p #IH <tr_id_unfold <tr_pap_succ //
+#p >(tr_pushs_id p)
+/2 width=1 by tr_pap_pushs_le/
qed.