X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsubstitution%2Flift_prototerm.ma;h=9193260452841583ff83da63e3f76f9c72a68ff5;hb=2cc4eb5d0210be58286e028278852122dcb68052;hp=708e8a82cbb9f09aa0d82d42644399cea8d43939;hpb=513a56a5990201abcf038e7242779e2d73621c86;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm.ma
index 708e8a82c..919326045 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm.ma
@@ -21,3 +21,9 @@ include "ground/lib/subset_ext_equivalence.ma".
 interpretation
   "lift (prototerm)"
   'UpArrow f t = (subset_ext_f1 ? ? (lift_gen ? proj_path f) t).
+
+(* Basic constructions ******************************************************)
+
+lemma in_comp_lift_bi (f) (p) (t):
+      p ϵ t → ↑[f]p ϵ ↑[f]t.
+/2 width=1 by subset_in_ext_f1_dx/ qed.