]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_rmap_id.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / substitution / prelift_rmap_id.ma
index 0842044d34ad36afdcbacbe70b15978911c3da4e..2f3c4ad8025b287e04ebb0d51535be453bdc9dbe 100644 (file)
@@ -20,6 +20,6 @@ include "ground/relocation/tr_id_tls.ma".
 (* Constructions with tr_id *************************************************)
 
 lemma prelift_rmap_id (l):
-      (𝐢) = ↑[l]𝐢.
+      (𝐢) = 🠢[𝐢]l.
 * [ #k ] //
 qed.