update in ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / tr_uni.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni.ma
index b57b05a949ba93eaf863aba5aa0aa278994da282..f5c60d12f5959536c2fe72b818ed6467f3883c21 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni.ma
@@ -26,6 +26,9 @@ interpretation
 
 (* Basic constructions ******************************************************)
 
+lemma tr_uni_unfold (n): ↑n ⨮ 𝐢 = 𝐮❨n❩.
+// qed.
+
 lemma tr_uni_zero: 𝐢 = 𝐮❨𝟎❩.
 <tr_id_unfold //
 qed.