X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fsubstitution%2Flift.ma;h=622f4ef531db3ecc0b5b5440e7187e6579d224b1;hb=fec1a061eeca5e7e05b4f0c3e299983b163569c3;hp=cb8aac3a00ccd2c676a4fba4eccf6009ed572513;hpb=eb918fc784eacd2094e3986ba321ef47690d9983;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 cb8aac3a0..622f4ef53 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Basic_2/grammar/term_weight.ma".
-include "Basic_2/grammar/term_simple.ma".
+include "basic_2/grammar/term_weight.ma".
+include "basic_2/grammar/term_simple.ma".
 
 (* BASIC TERM RELOCATION ****************************************************)
 
@@ -171,7 +171,7 @@ qed-.
 
 (* Basic_1: was: lift_gen_lref_false *)
 lemma lift_inv_lref2_be: ∀d,e,T1,i. ⇧[d,e] T1 ≡ #i →
-                         d ≤ i → i < d + e → False.
+                         d ≤ i → i < d + e → ⊥.
 #d #e #T1 #i #H elim (lift_inv_lref2 … H) -H *
 [ #H1 #_ #H2 #_ | #H2 #_ #_ #H1 ]
 lapply (le_to_lt_to_lt … H2 H1) -H2 -H1 #H
@@ -237,7 +237,7 @@ lemma lift_inv_flat2: ∀d,e,T1,I,V2,U2. ⇧[d,e] T1 ≡  ⓕ{I} V2. U2 →
                                T1 = ⓕ{I} V1. U1.
 /2 width=3/ qed-.
 
-lemma lift_inv_pair_xy_x: ∀d,e,I,V,T. ⇧[d, e] ②{I} V. T ≡ V → False.
+lemma lift_inv_pair_xy_x: ∀d,e,I,V,T. ⇧[d, e] ②{I} V. T ≡ V → ⊥.
 #d #e #J #V elim V -V
 [ * #i #T #H
   [ lapply (lift_inv_sort2 … H) -H #H destruct
@@ -251,7 +251,7 @@ lemma lift_inv_pair_xy_x: ∀d,e,I,V,T. ⇧[d, e] ②{I} V. T ≡ V → False.
 ]
 qed-.
 
-lemma lift_inv_pair_xy_y: ∀I,T,V,d,e. ⇧[d, e] ②{I} V. T ≡ T → False.
+lemma lift_inv_pair_xy_y: ∀I,T,V,d,e. ⇧[d, e] ②{I} V. T ≡ T → ⊥.
 #J #T elim T -T
 [ * #i #V #d #e #H
   [ lapply (lift_inv_sort2 … H) -H #H destruct
@@ -271,13 +271,13 @@ 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].
+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].
+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)