- new component "s_transition" for the restored fqu and fquq

[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 06223bc534baba0a840088c7471c56d3733b719f..a1f191a2586e98896ca9db07831e3d2793136645 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "ground_2/notation/relations/rat_3.ma".
-include "ground_2/relocation/rtmap_id.ma".
+include "ground_2/relocation/rtmap_uni.ma".
 
 (* RELOCATION MAP ***********************************************************)
 
@@ -320,3 +320,9 @@ lemma id_inv_at: ∀f. (∀i. @⦃i, f⦄ ≡ i) → 𝐈𝐝 ≗ f.
 
 lemma id_at: ∀i. @⦃i, 𝐈𝐝⦄ ≡ i.
 /2 width=1 by isid_inv_at/ qed.
+
+(* Properties with uniform relocations **************************************)
+
+lemma at_uni: ∀n,i. @⦃i,𝐔❴n❵⦄ ≡ n+i.
+#n elim n -n /2 width=5 by at_next/
+qed.