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 "apps_2/functional/flifts_flifts.ma".
16 include "apps_2/functional/flifts_basic.ma".
18 (* BASIC FUNCTIONAL RELOCATION **********************************************)
20 (* Main properties **********************************************************)
22 theorem flifts_basic_swap (T) (d1) (d2) (h1) (h2):
23 d2 ≤ d1 → ↑[d2,h2]↑[d1,h1]T = ↑[h2+d1,h1]↑[d2,h2]T.
24 /3 width=1 by flifts_comp, basic_swap/ qed-.
26 lemma flift_join: ∀e1,e2,T. ⇧[e1,e2] ↑[0,e1] T ≡ ↑[0,e1 + e2] T.
28 lapply (flift_lift T 0 (e1+e2)) #H
29 elim (lift_split … H e1 e1) -H // #U #H
30 >(flift_inv_lift … H) -H //