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 "delayed_updating/substitution/lift_gen_eq.ma".
16 include "delayed_updating/substitution/prelift_label.ma".
17 include "delayed_updating/substitution/prelift_rmap.ma".
19 (* LIFT FOR PATH ************************************************************)
21 (* Constructions with prelift_rmap and prelift_path *************************)
23 lemma lift_path_lcons_prelift (f) (p) (l):
24 (↑[f]l)◗↑[↑[l]f]p = ↑[f](l◗p).
28 lemma lift_path_rcons_prelift (f) (p) (l):
29 (↑[f]p)◖↑[↑[p]f]l = ↑[f](p◖l).