X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Frtmap_isid.ma;h=65e111bbf9d3e209bbb6516965ff215c934dd339;hb=66962864d3703b8f3b44e95d32c03ed50ceee6f1;hp=d713c1618f048967f1af54cc1e96635a88821738;hpb=87d9d5e65251b91b9d77c8f67069008dcec919d4;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma
index d713c1618..65e111bbf 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma
@@ -75,6 +75,18 @@ corec lemma eq_push_inv_isid: ∀f. 𝐈⦃f⦄ → ↑f ≗ f.
 @eq_f //
 qed-.
 
+(* Properties with iterated push ********************************************)
+
+lemma isid_pushs: ∀n,f. 𝐈⦃f⦄ → 𝐈⦃↑*[n]f⦄.
+#n elim n -n /3 width=3 by isid_push/
+qed.
+
+(* Inversion lemmas with iterated push **************************************)
+
+lemma isid_inv_pushs: ∀n,g. 𝐈⦃↑*[n]g⦄ → 𝐈⦃g⦄.
+#n elim n -n /3 width=3 by isid_inv_push/
+qed.
+
 (* Properties with tail *****************************************************)
 
 lemma isid_tl: ∀f. 𝐈⦃f⦄ → 𝐈⦃⫱f⦄.