(* 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
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
]
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
#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)