work in progress on frees_drops

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

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma
index 90e73d347f4de952566bf8293abd4e3f38b48d04..4af66a1c25f92f256567c6e617faa0a648b6937a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma
@@ -385,3 +385,8 @@ theorem at_div_id_sn: ∀f. H_at_div 𝐈𝐝 f f 𝐈𝐝.
 lemma at_uni: ∀n,i. @⦃i,𝐔❴n❵⦄ ≡ n+i.
 #n elim n -n /2 width=5 by at_next/
 qed.
+
+(* Inversion lemmas with uniform relocations ********************************)
+
+lemma at_inv_uni: ∀n,i,j. @⦃i,𝐔❴n❵⦄ ≡ j → j = n+i.
+/2 width=4 by at_mono/ qed-.