update in ground

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / substitution / lift_id.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_id.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_id.ma
index 1d8b45295c1b19d593917d915e4680a51f7eeeb3..c2376b52e4562b3db54cf5404af88fae2122bc14 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_id.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_id.ma
@@ -16,9 +16,9 @@ include "delayed_updating/substitution/lift_eq.ma".
 include "ground/relocation/tr_id_pap.ma".
 include "ground/relocation/tr_id_tls.ma".
 
-(* LIFT FOR PATH ***********************************************************)
+(* LIFT FOR PATH ************************************************************)
 
-(* Constructions with tr_id ************************************************)
+(* Constructions with proj_path and tr_id ***********************************)
 
 lemma lift_path_id (p):
       p = ↑[𝐢]p.
@@ -28,3 +28,11 @@ lemma lift_path_id (p):
 | <lift_path_L_sn //
 ]
 qed.
+
+(* Constructions with proj_rmap and tr_id ***********************************)
+
+lemma lift_rmap_id (p):
+      (𝐢) = ↑[p]𝐢.
+#p elim p -p //
+* [ #n ] #p #IH //
+qed.