the support for reducibility candidates evolves ,,,,

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / substitution / lift.ma

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 9e6b261c816defa2c26854dd4f664e2e95a7cbc5..0e0e6a7483158ff98819cbb2a9ec3b7a57d66a6d 100644 (file)
--- 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 *)