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 "static_2/relocation/lifts_lifts.ma".
16 include "apps_2/functional/flifts.ma".
18 (* GENERIC FUNCTIONAL RELOCATION ********************************************)
20 (* Main derived properties **************************************************)
22 theorem flifts_compose (f2) (f1) (T): ↑*[f2]↑*[f1]T = ↑*[f2∘f1]T.
24 elim (lifts_total T f1) #U #HTU
25 >(flifts_inv_lifts … HTU)
26 /4 width=6 by flifts_inv_lifts, lifts_trans, sym_eq/
29 (* Main derived properties with uniform relocation **************************)
31 theorem flifts_compose_uni (l2) (l1) (T): ↑[l2]↑[l1]T = ↑[l2+l1]T.
32 #l2 #l1 #T >flifts_compose
33 /4 width=1 by flifts_inv_lifts, lifts_uni, sym_eq/ qed.