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 "ground_2/relocation/nstream_after.ma".
16 include "static_2/notation/relations/rliftstar_3.ma".
17 include "static_2/syntax/term.ma".
19 (* GENERIC RELOCATION FOR TERMS *********************************************)
22 lift_sort lift_lref_lt lift_lref_ge lift_bind lift_flat
25 inductive lifts: rtmap → relation term ≝
26 | lifts_sort: ∀f,s. lifts f (⋆s) (⋆s)
27 | lifts_lref: ∀f,i1,i2. @⦃i1, f⦄ ≘ i2 → lifts f (#i1) (#i2)
28 | lifts_gref: ∀f,l. lifts f (§l) (§l)
29 | lifts_bind: ∀f,p,I,V1,V2,T1,T2.
30 lifts f V1 V2 → lifts (⫯f) T1 T2 →
31 lifts f (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
32 | lifts_flat: ∀f,I,V1,V2,T1,T2.
33 lifts f V1 V2 → lifts f T1 T2 →
34 lifts f (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
37 interpretation "uniform relocation (term)"
38 'RLiftStar i T1 T2 = (lifts (uni i) T1 T2).
40 interpretation "generic relocation (term)"
41 'RLiftStar f T1 T2 = (lifts f T1 T2).
43 definition liftable2_sn: predicate (relation term) ≝
44 λR. ∀T1,T2. R T1 T2 → ∀f,U1. ⬆*[f] T1 ≘ U1 →
45 ∃∃U2. ⬆*[f] T2 ≘ U2 & R U1 U2.
47 definition deliftable2_sn: predicate (relation term) ≝
48 λR. ∀U1,U2. R U1 U2 → ∀f,T1. ⬆*[f] T1 ≘ U1 →
49 ∃∃T2. ⬆*[f] T2 ≘ U2 & R T1 T2.
51 definition liftable2_bi: predicate (relation term) ≝
52 λR. ∀T1,T2. R T1 T2 → ∀f,U1. ⬆*[f] T1 ≘ U1 →
53 ∀U2. ⬆*[f] T2 ≘ U2 → R U1 U2.
55 definition deliftable2_bi: predicate (relation term) ≝
56 λR. ∀U1,U2. R U1 U2 → ∀f,T1. ⬆*[f] T1 ≘ U1 →
57 ∀T2. ⬆*[f] T2 ≘ U2 → R T1 T2.
59 definition deliftable2_dx: predicate (relation term) ≝
60 λR. ∀U1,U2. R U1 U2 → ∀f,T2. ⬆*[f] T2 ≘ U2 →
61 ∃∃T1. ⬆*[f] T1 ≘ U1 & R T1 T2.
63 (* Basic inversion lemmas ***************************************************)
65 fact lifts_inv_sort1_aux: ∀f,X,Y. ⬆*[f] X ≘ Y → ∀s. X = ⋆s → Y = ⋆s.
66 #f #X #Y * -f -X -Y //
67 [ #f #i1 #i2 #_ #x #H destruct
68 | #f #p #I #V1 #V2 #T1 #T2 #_ #_ #x #H destruct
69 | #f #I #V1 #V2 #T1 #T2 #_ #_ #x #H destruct
73 (* Basic_1: was: lift1_sort *)
74 (* Basic_2A1: includes: lift_inv_sort1 *)
75 lemma lifts_inv_sort1: ∀f,Y,s. ⬆*[f] ⋆s ≘ Y → Y = ⋆s.
76 /2 width=4 by lifts_inv_sort1_aux/ qed-.
78 fact lifts_inv_lref1_aux: ∀f,X,Y. ⬆*[f] X ≘ Y → ∀i1. X = #i1 →
79 ∃∃i2. @⦃i1, f⦄ ≘ i2 & Y = #i2.
81 [ #f #s #x #H destruct
82 | #f #i1 #i2 #Hi12 #x #H destruct /2 width=3 by ex2_intro/
83 | #f #l #x #H destruct
84 | #f #p #I #V1 #V2 #T1 #T2 #_ #_ #x #H destruct
85 | #f #I #V1 #V2 #T1 #T2 #_ #_ #x #H destruct
89 (* Basic_1: was: lift1_lref *)
90 (* Basic_2A1: includes: lift_inv_lref1 lift_inv_lref1_lt lift_inv_lref1_ge *)
91 lemma lifts_inv_lref1: ∀f,Y,i1. ⬆*[f] #i1 ≘ Y →
92 ∃∃i2. @⦃i1, f⦄ ≘ i2 & Y = #i2.
93 /2 width=3 by lifts_inv_lref1_aux/ qed-.
95 fact lifts_inv_gref1_aux: ∀f,X,Y. ⬆*[f] X ≘ Y → ∀l. X = §l → Y = §l.
96 #f #X #Y * -f -X -Y //
97 [ #f #i1 #i2 #_ #x #H destruct
98 | #f #p #I #V1 #V2 #T1 #T2 #_ #_ #x #H destruct
99 | #f #I #V1 #V2 #T1 #T2 #_ #_ #x #H destruct
103 (* Basic_2A1: includes: lift_inv_gref1 *)
104 lemma lifts_inv_gref1: ∀f,Y,l. ⬆*[f] §l ≘ Y → Y = §l.
105 /2 width=4 by lifts_inv_gref1_aux/ qed-.
107 fact lifts_inv_bind1_aux: ∀f,X,Y. ⬆*[f] X ≘ Y →
108 ∀p,I,V1,T1. X = ⓑ{p,I}V1.T1 →
109 ∃∃V2,T2. ⬆*[f] V1 ≘ V2 & ⬆*[⫯f] T1 ≘ T2 &
112 [ #f #s #q #J #W1 #U1 #H destruct
113 | #f #i1 #i2 #_ #q #J #W1 #U1 #H destruct
114 | #f #l #b #J #W1 #U1 #H destruct
115 | #f #p #I #V1 #V2 #T1 #T2 #HV12 #HT12 #q #J #W1 #U1 #H destruct /2 width=5 by ex3_2_intro/
116 | #f #I #V1 #V2 #T1 #T2 #_ #_ #q #J #W1 #U1 #H destruct
120 (* Basic_1: was: lift1_bind *)
121 (* Basic_2A1: includes: lift_inv_bind1 *)
122 lemma lifts_inv_bind1: ∀f,p,I,V1,T1,Y. ⬆*[f] ⓑ{p,I}V1.T1 ≘ Y →
123 ∃∃V2,T2. ⬆*[f] V1 ≘ V2 & ⬆*[⫯f] T1 ≘ T2 &
125 /2 width=3 by lifts_inv_bind1_aux/ qed-.
127 fact lifts_inv_flat1_aux: ∀f:rtmap. ∀X,Y. ⬆*[f] X ≘ Y →
128 ∀I,V1,T1. X = ⓕ{I}V1.T1 →
129 ∃∃V2,T2. ⬆*[f] V1 ≘ V2 & ⬆*[f] T1 ≘ T2 &
132 [ #f #s #J #W1 #U1 #H destruct
133 | #f #i1 #i2 #_ #J #W1 #U1 #H destruct
134 | #f #l #J #W1 #U1 #H destruct
135 | #f #p #I #V1 #V2 #T1 #T2 #_ #_ #J #W1 #U1 #H destruct
136 | #f #I #V1 #V2 #T1 #T2 #HV12 #HT12 #J #W1 #U1 #H destruct /2 width=5 by ex3_2_intro/
140 (* Basic_1: was: lift1_flat *)
141 (* Basic_2A1: includes: lift_inv_flat1 *)
142 lemma lifts_inv_flat1: ∀f:rtmap. ∀I,V1,T1,Y. ⬆*[f] ⓕ{I}V1.T1 ≘ Y →
143 ∃∃V2,T2. ⬆*[f] V1 ≘ V2 & ⬆*[f] T1 ≘ T2 &
145 /2 width=3 by lifts_inv_flat1_aux/ qed-.
147 fact lifts_inv_sort2_aux: ∀f,X,Y. ⬆*[f] X ≘ Y → ∀s. Y = ⋆s → X = ⋆s.
148 #f #X #Y * -f -X -Y //
149 [ #f #i1 #i2 #_ #x #H destruct
150 | #f #p #I #V1 #V2 #T1 #T2 #_ #_ #x #H destruct
151 | #f #I #V1 #V2 #T1 #T2 #_ #_ #x #H destruct
155 (* Basic_1: includes: lift_gen_sort *)
156 (* Basic_2A1: includes: lift_inv_sort2 *)
157 lemma lifts_inv_sort2: ∀f,X,s. ⬆*[f] X ≘ ⋆s → X = ⋆s.
158 /2 width=4 by lifts_inv_sort2_aux/ qed-.
160 fact lifts_inv_lref2_aux: ∀f,X,Y. ⬆*[f] X ≘ Y → ∀i2. Y = #i2 →
161 ∃∃i1. @⦃i1, f⦄ ≘ i2 & X = #i1.
163 [ #f #s #x #H destruct
164 | #f #i1 #i2 #Hi12 #x #H destruct /2 width=3 by ex2_intro/
165 | #f #l #x #H destruct
166 | #f #p #I #V1 #V2 #T1 #T2 #_ #_ #x #H destruct
167 | #f #I #V1 #V2 #T1 #T2 #_ #_ #x #H destruct
171 (* Basic_1: includes: lift_gen_lref lift_gen_lref_lt lift_gen_lref_false lift_gen_lref_ge *)
172 (* Basic_2A1: includes: lift_inv_lref2 lift_inv_lref2_lt lift_inv_lref2_be lift_inv_lref2_ge lift_inv_lref2_plus *)
173 lemma lifts_inv_lref2: ∀f,X,i2. ⬆*[f] X ≘ #i2 →
174 ∃∃i1. @⦃i1, f⦄ ≘ i2 & X = #i1.
175 /2 width=3 by lifts_inv_lref2_aux/ qed-.
177 fact lifts_inv_gref2_aux: ∀f,X,Y. ⬆*[f] X ≘ Y → ∀l. Y = §l → X = §l.
178 #f #X #Y * -f -X -Y //
179 [ #f #i1 #i2 #_ #x #H destruct
180 | #f #p #I #V1 #V2 #T1 #T2 #_ #_ #x #H destruct
181 | #f #I #V1 #V2 #T1 #T2 #_ #_ #x #H destruct
185 (* Basic_2A1: includes: lift_inv_gref1 *)
186 lemma lifts_inv_gref2: ∀f,X,l. ⬆*[f] X ≘ §l → X = §l.
187 /2 width=4 by lifts_inv_gref2_aux/ qed-.
189 fact lifts_inv_bind2_aux: ∀f,X,Y. ⬆*[f] X ≘ Y →
190 ∀p,I,V2,T2. Y = ⓑ{p,I}V2.T2 →
191 ∃∃V1,T1. ⬆*[f] V1 ≘ V2 & ⬆*[⫯f] T1 ≘ T2 &
194 [ #f #s #q #J #W2 #U2 #H destruct
195 | #f #i1 #i2 #_ #q #J #W2 #U2 #H destruct
196 | #f #l #q #J #W2 #U2 #H destruct
197 | #f #p #I #V1 #V2 #T1 #T2 #HV12 #HT12 #q #J #W2 #U2 #H destruct /2 width=5 by ex3_2_intro/
198 | #f #I #V1 #V2 #T1 #T2 #_ #_ #q #J #W2 #U2 #H destruct
202 (* Basic_1: includes: lift_gen_bind *)
203 (* Basic_2A1: includes: lift_inv_bind2 *)
204 lemma lifts_inv_bind2: ∀f,p,I,V2,T2,X. ⬆*[f] X ≘ ⓑ{p,I}V2.T2 →
205 ∃∃V1,T1. ⬆*[f] V1 ≘ V2 & ⬆*[⫯f] T1 ≘ T2 &
207 /2 width=3 by lifts_inv_bind2_aux/ qed-.
209 fact lifts_inv_flat2_aux: ∀f:rtmap. ∀X,Y. ⬆*[f] X ≘ Y →
210 ∀I,V2,T2. Y = ⓕ{I}V2.T2 →
211 ∃∃V1,T1. ⬆*[f] V1 ≘ V2 & ⬆*[f] T1 ≘ T2 &
214 [ #f #s #J #W2 #U2 #H destruct
215 | #f #i1 #i2 #_ #J #W2 #U2 #H destruct
216 | #f #l #J #W2 #U2 #H destruct
217 | #f #p #I #V1 #V2 #T1 #T2 #_ #_ #J #W2 #U2 #H destruct
218 | #f #I #V1 #V2 #T1 #T2 #HV12 #HT12 #J #W2 #U2 #H destruct /2 width=5 by ex3_2_intro/
222 (* Basic_1: includes: lift_gen_flat *)
223 (* Basic_2A1: includes: lift_inv_flat2 *)
224 lemma lifts_inv_flat2: ∀f:rtmap. ∀I,V2,T2,X. ⬆*[f] X ≘ ⓕ{I}V2.T2 →
225 ∃∃V1,T1. ⬆*[f] V1 ≘ V2 & ⬆*[f] T1 ≘ T2 &
227 /2 width=3 by lifts_inv_flat2_aux/ qed-.
229 (* Advanced inversion lemmas ************************************************)
231 lemma lifts_inv_atom1: ∀f,I,Y. ⬆*[f] ⓪{I} ≘ Y →
232 ∨∨ ∃∃s. I = Sort s & Y = ⋆s
233 | ∃∃i,j. @⦃i, f⦄ ≘ j & I = LRef i & Y = #j
234 | ∃∃l. I = GRef l & Y = §l.
236 [ lapply (lifts_inv_sort1 … H)
237 | elim (lifts_inv_lref1 … H)
238 | lapply (lifts_inv_gref1 … H)
239 ] -H /3 width=5 by or3_intro0, or3_intro1, or3_intro2, ex3_2_intro, ex2_intro/
242 lemma lifts_inv_atom2: ∀f,I,X. ⬆*[f] X ≘ ⓪{I} →
243 ∨∨ ∃∃s. X = ⋆s & I = Sort s
244 | ∃∃i,j. @⦃i, f⦄ ≘ j & X = #i & I = LRef j
245 | ∃∃l. X = §l & I = GRef l.
247 [ lapply (lifts_inv_sort2 … H)
248 | elim (lifts_inv_lref2 … H)
249 | lapply (lifts_inv_gref2 … H)
250 ] -H /3 width=5 by or3_intro0, or3_intro1, or3_intro2, ex3_2_intro, ex2_intro/
253 (* Basic_2A1: includes: lift_inv_pair_xy_x *)
254 lemma lifts_inv_pair_xy_x: ∀f,I,V,T. ⬆*[f] ②{I}V.T ≘ V → ⊥.
257 [ lapply (lifts_inv_sort2 … H) -H #H destruct
258 | elim (lifts_inv_lref2 … H) -H
260 | lapply (lifts_inv_gref2 … H) -H #H destruct
262 | * [ #p ] #I #V2 #T2 #IHV2 #_ #U #H
263 [ elim (lifts_inv_bind2 … H) -H #V1 #T1 #HV12 #_ #H destruct /2 width=3 by/
264 | elim (lifts_inv_flat2 … H) -H #V1 #T1 #HV12 #_ #H destruct /2 width=3 by/
269 (* Basic_1: includes: thead_x_lift_y_y *)
270 (* Basic_2A1: includes: lift_inv_pair_xy_y *)
271 lemma lifts_inv_pair_xy_y: ∀I,T,V,f. ⬆*[f] ②{I}V.T ≘ T → ⊥.
274 [ lapply (lifts_inv_sort2 … H) -H #H destruct
275 | elim (lifts_inv_lref2 … H) -H
277 | lapply (lifts_inv_gref2 … H) -H #H destruct
279 | * [ #p ] #I #V2 #T2 #_ #IHT2 #W #f #H
280 [ elim (lifts_inv_bind2 … H) -H #V1 #T1 #_ #HT12 #H destruct /2 width=4 by/
281 | elim (lifts_inv_flat2 … H) -H #V1 #T1 #_ #HT12 #H destruct /2 width=4 by/
286 (* Inversion lemmas with uniform relocations ********************************)
288 lemma lifts_inv_lref1_uni: ∀l,Y,i. ⬆*[l] #i ≘ Y → Y = #(l+i).
289 #l #Y #i1 #H elim (lifts_inv_lref1 … H) -H /4 width=4 by at_mono, eq_f/
292 lemma lifts_inv_lref2_uni: ∀l,X,i2. ⬆*[l] X ≘ #i2 →
293 ∃∃i1. X = #i1 & i2 = l + i1.
294 #l #X #i2 #H elim (lifts_inv_lref2 … H) -H
295 /3 width=3 by at_inv_uni, ex2_intro/
298 lemma lifts_inv_lref2_uni_ge: ∀l,X,i. ⬆*[l] X ≘ #(l + i) → X = #i.
299 #l #X #i2 #H elim (lifts_inv_lref2_uni … H) -H
300 #i1 #H1 #H2 destruct /4 width=2 by injective_plus_r, eq_f, sym_eq/
303 lemma lifts_inv_lref2_uni_lt: ∀l,X,i. ⬆*[l] X ≘ #i → i < l → ⊥.
304 #l #X #i2 #H elim (lifts_inv_lref2_uni … H) -H
305 #i1 #_ #H1 #H2 destruct /2 width=4 by lt_le_false/
308 (* Basic forward lemmas *****************************************************)
310 (* Basic_2A1: includes: lift_inv_O2 *)
311 lemma lifts_fwd_isid: ∀f,T1,T2. ⬆*[f] T1 ≘ T2 → 𝐈⦃f⦄ → T1 = T2.
312 #f #T1 #T2 #H elim H -f -T1 -T2
313 /4 width=3 by isid_inv_at_mono, isid_push, eq_f2, eq_f/
316 (* Basic_2A1: includes: lift_fwd_pair1 *)
317 lemma lifts_fwd_pair1: ∀f:rtmap. ∀I,V1,T1,Y. ⬆*[f] ②{I}V1.T1 ≘ Y →
318 ∃∃V2,T2. ⬆*[f] V1 ≘ V2 & Y = ②{I}V2.T2.
319 #f * [ #p ] #I #V1 #T1 #Y #H
320 [ elim (lifts_inv_bind1 … H) -H /2 width=4 by ex2_2_intro/
321 | elim (lifts_inv_flat1 … H) -H /2 width=4 by ex2_2_intro/
325 (* Basic_2A1: includes: lift_fwd_pair2 *)
326 lemma lifts_fwd_pair2: ∀f:rtmap. ∀I,V2,T2,X. ⬆*[f] X ≘ ②{I}V2.T2 →
327 ∃∃V1,T1. ⬆*[f] V1 ≘ V2 & X = ②{I}V1.T1.
328 #f * [ #p ] #I #V2 #T2 #X #H
329 [ elim (lifts_inv_bind2 … H) -H /2 width=4 by ex2_2_intro/
330 | elim (lifts_inv_flat2 … H) -H /2 width=4 by ex2_2_intro/
334 (* Basic properties *********************************************************)
336 lemma deliftable2_sn_dx (R): symmetric … R → deliftable2_sn R → deliftable2_dx R.
337 #R #H2R #H1R #U1 #U2 #HU12 #f #T2 #HTU2
338 elim (H1R … U1 … HTU2) -H1R /3 width=3 by ex2_intro/
341 lemma lifts_eq_repl_back: ∀T1,T2. eq_repl_back … (λf. ⬆*[f] T1 ≘ T2).
342 #T1 #T2 #f1 #H elim H -T1 -T2 -f1
343 /4 width=5 by lifts_flat, lifts_bind, lifts_lref, at_eq_repl_back, eq_push/
346 lemma lifts_eq_repl_fwd: ∀T1,T2. eq_repl_fwd … (λf. ⬆*[f] T1 ≘ T2).
347 #T1 #T2 @eq_repl_sym /2 width=3 by lifts_eq_repl_back/ (**) (* full auto fails *)
350 (* Basic_1: includes: lift_r *)
351 (* Basic_2A1: includes: lift_refl *)
352 lemma lifts_refl: ∀T,f. 𝐈⦃f⦄ → ⬆*[f] T ≘ T.
354 /4 width=3 by lifts_flat, lifts_bind, lifts_lref, isid_inv_at, isid_push/
357 (* Basic_2A1: includes: lift_total *)
358 lemma lifts_total: ∀T1,f. ∃T2. ⬆*[f] T1 ≘ T2.
360 /3 width=2 by lifts_lref, lifts_sort, lifts_gref, ex_intro/
361 [ #p ] #I #V1 #T1 #IHV1 #IHT1 #f
362 elim (IHV1 f) -IHV1 #V2 #HV12
363 [ elim (IHT1 (⫯f)) -IHT1 /3 width=2 by lifts_bind, ex_intro/
364 | elim (IHT1 f) -IHT1 /3 width=2 by lifts_flat, ex_intro/
368 lemma lifts_push_zero (f): ⬆*[⫯f]#O ≘ #0.
369 /2 width=1 by lifts_lref/ qed.
371 lemma lifts_push_lref (f) (i1) (i2): ⬆*[f]#i1 ≘ #i2 → ⬆*[⫯f]#(↑i1) ≘ #(↑i2).
373 elim (lifts_inv_lref1 … H) -H #j #Hij #H destruct
374 /3 width=7 by lifts_lref, at_push/
377 lemma lifts_lref_uni: ∀l,i. ⬆*[l] #i ≘ #(l+i).
378 #l elim l -l /2 width=1 by lifts_lref/
381 (* Basic_1: includes: lift_free (right to left) *)
382 (* Basic_2A1: includes: lift_split *)
383 lemma lifts_split_trans: ∀f,T1,T2. ⬆*[f] T1 ≘ T2 →
384 ∀f1,f2. f2 ⊚ f1 ≘ f →
385 ∃∃T. ⬆*[f1] T1 ≘ T & ⬆*[f2] T ≘ T2.
386 #f #T1 #T2 #H elim H -f -T1 -T2
387 [ /3 width=3 by lifts_sort, ex2_intro/
388 | #f #i1 #i2 #Hi #f1 #f2 #Ht elim (after_at_fwd … Hi … Ht) -Hi -Ht
389 /3 width=3 by lifts_lref, ex2_intro/
390 | /3 width=3 by lifts_gref, ex2_intro/
391 | #f #p #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f1 #f2 #Ht
392 elim (IHV … Ht) elim (IHT (⫯f1) (⫯f2)) -IHV -IHT
393 /3 width=5 by lifts_bind, after_O2, ex2_intro/
394 | #f #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f1 #f2 #Ht
395 elim (IHV … Ht) elim (IHT … Ht) -IHV -IHT -Ht
396 /3 width=5 by lifts_flat, ex2_intro/
400 (* Note: apparently, this was missing in Basic_2A1 *)
401 lemma lifts_split_div: ∀f1,T1,T2. ⬆*[f1] T1 ≘ T2 →
403 ∃∃T. ⬆*[f2] T2 ≘ T & ⬆*[f] T1 ≘ T.
404 #f1 #T1 #T2 #H elim H -f1 -T1 -T2
405 [ /3 width=3 by lifts_sort, ex2_intro/
406 | #f1 #i1 #i2 #Hi #f2 #f #Ht elim (after_at1_fwd … Hi … Ht) -Hi -Ht
407 /3 width=3 by lifts_lref, ex2_intro/
408 | /3 width=3 by lifts_gref, ex2_intro/
409 | #f1 #p #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f2 #f #Ht
410 elim (IHV … Ht) elim (IHT (⫯f2) (⫯f)) -IHV -IHT
411 /3 width=5 by lifts_bind, after_O2, ex2_intro/
412 | #f1 #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f2 #f #Ht
413 elim (IHV … Ht) elim (IHT … Ht) -IHV -IHT -Ht
414 /3 width=5 by lifts_flat, ex2_intro/
418 (* Basic_1: includes: dnf_dec2 dnf_dec *)
419 (* Basic_2A1: includes: is_lift_dec *)
420 lemma is_lifts_dec: ∀T2,f. Decidable (∃T1. ⬆*[f] T1 ≘ T2).
422 [ * [1,3: /3 width=2 by lifts_sort, lifts_gref, ex_intro, or_introl/ ]
423 #i2 #f elim (is_at_dec f i2) //
424 [ * /4 width=3 by lifts_lref, ex_intro, or_introl/
426 #X #HX elim (lifts_inv_lref2 … HX) -HX
427 /3 width=2 by ex_intro/
429 | * [ #p ] #I #V2 #T2 #IHV2 #IHT2 #f
430 [ elim (IHV2 f) -IHV2
431 [ * #V1 #HV12 elim (IHT2 (⫯f)) -IHT2
432 [ * #T1 #HT12 @or_introl /3 width=2 by lifts_bind, ex_intro/
433 | -V1 #HT2 @or_intror * #X #H
434 elim (lifts_inv_bind2 … H) -H /3 width=2 by ex_intro/
436 | -IHT2 #HV2 @or_intror * #X #H
437 elim (lifts_inv_bind2 … H) -H /3 width=2 by ex_intro/
439 | elim (IHV2 f) -IHV2
440 [ * #V1 #HV12 elim (IHT2 f) -IHT2
441 [ * #T1 #HT12 /4 width=2 by lifts_flat, ex_intro, or_introl/
442 | -V1 #HT2 @or_intror * #X #H
443 elim (lifts_inv_flat2 … H) -H /3 width=2 by ex_intro/
445 | -IHT2 #HV2 @or_intror * #X #H
446 elim (lifts_inv_flat2 … H) -H /3 width=2 by ex_intro/
452 (* Properties with uniform relocation ***************************************)
454 lemma lifts_uni: ∀n1,n2,T,U. ⬆*[𝐔❴n1❵∘𝐔❴n2❵] T ≘ U → ⬆*[n1+n2] T ≘ U.
455 /3 width=4 by lifts_eq_repl_back, after_inv_total/ qed.
457 (* Basic_2A1: removed theorems 14:
458 lifts_inv_nil lifts_inv_cons
459 lift_inv_Y1 lift_inv_Y2 lift_inv_lref_Y1 lift_inv_lref_Y2 lift_lref_Y lift_Y1
460 lift_lref_lt_eq lift_lref_ge_eq lift_lref_plus lift_lref_pred
461 lift_lref_ge_minus lift_lref_ge_minus_eq
463 (* Basic_1: removed theorems 8:
465 lift_head lift_gen_head
466 lift_weight_map lift_weight lift_weight_add lift_weight_add_O