some results on co-composition ...

[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 7dde16d0f6472eaecab351bd21eebb8f75d58c53..d713c1618f048967f1af54cc1e96635a88821738 100644 (file)
--- 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,18 @@ 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 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.