- more results on relocation

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / relocation / rtmap_isid.ma

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 d713c1618f048967f1af54cc1e96635a88821738..65e111bbf9d3e209bbb6516965ff215c934dd339 100644 (file)
--- 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⦄.