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=528f8ea107f689d07d060e1d31ba32bf65b4e6ba;hp=7dde16d0f6472eaecab351bd21eebb8f75d58c53;hpb=5832735b721c0bd8567c8f0be761a9136363a2a6;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 7dde16d0f..65e111bbf 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma
@@ -74,3 +74,30 @@ corec lemma eq_push_inv_isid: ∀f. 𝐈⦃f⦄ → ↑f ≗ f.
 #f #g #Hf #Hg @(eq_push … Hg) [2: @eq_push_inv_isid // | skip ]
 @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⦄.
+#f cases (pn_split f) * #g * -f #H
+[ /2 width=3 by isid_inv_push/
+| elim (isid_inv_next … H) -H //
+]
+qed.
+
+(* Properties with iterated tail ********************************************)
+
+lemma isid_tls: ∀n,g. 𝐈⦃g⦄ → 𝐈⦃⫱*[n]g⦄.
+#n elim n -n /3 width=1 by isid_tl/
+qed.