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/syntax/path_structure.ma".
16 include "delayed_updating/substitution/lift_eq.ma".
18 (* LIFT FOR PATH ***********************************************************)
20 (* Constructions with structure ********************************************)
22 lemma lift_d_empty_dx (n) (p) (f):
23 (āp)āš±āØ(ā[p]f)@āØnā©ā© = ā[f](pāš±āØnā©).
24 #n #p @(path_ind_lift ā¦ p) -p // [ #m #l #p |*: #p ] #IH #f
25 [ <lift_rmap_d_sn <lift_path_d_lcons_sn //
26 | <lift_rmap_L_sn <lift_path_L_sn <IH //
27 | <lift_rmap_A_sn <lift_path_A_sn <IH //
28 | <lift_rmap_S_sn <lift_path_S_sn <IH //
32 lemma lift_L_dx (p) (f):
33 (āp)āš = ā[f](pāš).
34 #p @(path_ind_lift ā¦ p) -p // #m #l #p #IH #f
35 <lift_path_d_lcons_sn //
38 lemma lift_A_dx (p) (f):
39 (āp)āš = ā[f](pāš).
40 #p @(path_ind_lift ā¦ p) -p // #m #l #p #IH #f
41 <lift_path_d_lcons_sn //
44 lemma lift_S_dx (p) (f):
45 (āp)āš¦ = ā[f](pāš¦).
46 #p @(path_ind_lift ā¦ p) -p // #m #l #p #IH #f
47 <lift_path_d_lcons_sn //
50 lemma structure_lift (p) (f):
52 #p @(path_ind_lift ā¦ p) -p // #p #IH #f
56 lemma lift_structure (p) (f):
58 #p @(path_ind_lift ā¦ p) -p //