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/notation/functions/uptrianglearrow_2.ma".
16 include "delayed_updating/syntax/label.ma".
17 include "ground/relocation/tr_pap_pap.ma".
19 (* PRELIFT FOR LABEL ********************************************************)
21 definition prelift_label (f) (l): label ≝
23 [ label_d k ⇒ 𝗱(f@⧣❨k❩)
32 'UpTriangleArrow f l = (prelift_label f l).
34 (* Basic constructions ******************************************************)
36 lemma prelift_label_d (f) (k):
40 lemma prelift_label_m (f):
44 lemma prelift_label_L (f):
48 lemma prelift_label_A (f):
52 lemma prelift_label_S (f):
56 (* Basic inversions *********************************************************)
58 lemma prelift_label_inv_d_sn (f) (l) (k1):
60 ∃∃k2. k1 = f@⧣❨k2❩ & 𝗱k2 = l.
68 /2 width=3 by ex2_intro/
71 lemma prelift_label_inv_m_sn (f) (l):
82 lemma prelift_label_inv_L_sn (f) (l):
93 lemma prelift_label_inv_A_sn (f) (l):
104 lemma prelift_label_inv_S_sn (f) (l):
115 (* Main inversions **********************************************************)
117 theorem prelift_label_inj (f) (l1) (l2):
118 🠡[f]l1 = 🠡[f]l2 → l1 = l2.
120 [ elim (prelift_label_inv_d_sn … Hl) -Hl #k2 #Hk #H0 destruct
121 >(tr_pap_inj ???? Hk) -Hk //
122 | <(prelift_label_inv_m_sn … Hl) -l2 //
123 | <(prelift_label_inv_L_sn … Hl) -l2 //
124 | <(prelift_label_inv_A_sn … Hl) -l2 //
125 | <(prelift_label_inv_S_sn … Hl) -l2 //