1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "lambda-delta/substitution/lift_defs.ma".
17 (* RELOCATION ***************************************************************)
19 (* the functional properties ************************************************)
21 lemma lift_total: ∀T1,d,e. ∃T2. ↑[d,e] T1 ≡ T2.
24 | #i #d #e elim (lt_or_ge i d) /3/
25 | * #I #V1 #T1 #IHV1 #IHT1 #d #e
26 elim (IHV1 d e) -IHV1 #V2 #HV12
27 [ elim (IHT1 (d+1) e) -IHT1 /3/
28 | elim (IHT1 d e) -IHT1 /3/
33 lemma lift_mono: ∀d,e,T,U1. ↑[d,e] T ≡ U1 → ∀U2. ↑[d,e] T ≡ U2 → U1 = U2.
34 #d #e #T #U1 #H elim H -H d e T U1
36 lapply (lift_inv_sort1 … HX) -HX //
37 | #i #d #e #Hid #X #HX
38 lapply (lift_inv_lref1_lt … HX ?) -HX //
39 | #i #d #e #Hdi #X #HX
40 lapply (lift_inv_lref1_ge … HX ?) -HX //
41 | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
42 elim (lift_inv_bind1 … HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/
43 | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
44 elim (lift_inv_flat1 … HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/
48 lemma lift_inj: ∀d,e,T1,U. ↑[d,e] T1 ≡ U → ∀T2. ↑[d,e] T2 ≡ U → T1 = T2.
49 #d #e #T1 #U #H elim H -H d e T1 U
51 lapply (lift_inv_sort2 … HX) -HX //
52 | #i #d #e #Hid #X #HX
53 lapply (lift_inv_lref2_lt … HX ?) -HX //
54 | #i #d #e #Hdi #X #HX
55 lapply (lift_inv_lref2_ge … HX ?) -HX /2/
56 | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
57 elim (lift_inv_bind2 … HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/
58 | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
59 elim (lift_inv_flat2 … HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/