X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fsubstitution%2Flift.ma;h=0e0e6a7483158ff98819cbb2a9ec3b7a57d66a6d;hb=7e6643f9ce7ae87e9241aeac5b6d828e9d47fb63;hp=9e6b261c816defa2c26854dd4f664e2e95a7cbc5;hpb=2fef56731b0d38913967105495b96754e327efab;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma
index 9e6b261c8..0e0e6a748 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "Basic_2/grammar/term_weight.ma".
+include "Basic_2/grammar/term_simple.ma".
 
 (* RELOCATION ***************************************************************)
 
@@ -270,6 +271,18 @@ lemma tw_lift: ∀d,e,T1,T2. ⇑[d, e] T1 ≡ T2 → #[T1] = #[T2].
 #d #e #T1 #T2 #H elim H -d -e -T1 -T2 normalize //
 qed-.
 
+lemma lift_simple_dx: ∀d,e,T1,T2. ⇑[d, e] T1 ≡ T2 → 𝕊[T1] → 𝕊[T2].
+#d #e #T1 #T2 #H elim H -d -e -T1 -T2 //
+#I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #H
+elim (simple_inv_bind … H)
+qed-.
+
+lemma lift_simple_sn: ∀d,e,T1,T2. ⇑[d, e] T1 ≡ T2 → 𝕊[T2] → 𝕊[T1].
+#d #e #T1 #T2 #H elim H -d -e -T1 -T2 //
+#I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #H
+elim (simple_inv_bind … H)
+qed-. 
+
 (* Basic properties *********************************************************)
 
 (* Basic_1: was: lift_lref_gt *)