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 "lambda-delta/substitution/lift_main.ma".
16 include "lambda-delta/substitution/subst_defs.ma".
17 include "lambda-delta/reduction/pr_defs.ma".
19 lemma subst_pr: ∀d,e,L,T1,U2. L ⊢ ↓[d,e] T1 ≡ U2 → ∀T2. ↑[d,e] U2 ≡ T2 →
21 #d #e #L #T1 #U2 #H elim H -H d e L T1 U2
23 lapply (lift_inv_sort1 … HX) -HX #HX destruct -X //
24 | #L #i #d #e #Hid #X #HX
25 lapply (lift_inv_lref1_lt … HX Hid) -HX #HX destruct -X //
26 | #L #K #V #U1 #U2 #i #d #e #Hdi #Hide #HLK #_ #HU12 #IHVU1 #U #HU2
27 lapply (lift_trans_be … HU12 … HU2 ? ?) // -HU12 HU2 U2 #HU1
28 elim (lift_free … HU1 0 (d+e-i-1) ? ? ?) -HU1 // #U2 #HU12 >arith6 // #HU2
29 @pr_delta [4,5,6: /2/ |1,2,3: skip ] (**) (* /2/ *)
30 | #L #i #d #e #Hdei #X #HX
31 lapply (lift_inv_lref1_ge … HX ?) -HX /2/ #HX destruct -X;
33 | #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
34 elim (lift_inv_bind1 … HX) -HX #V #T #HV2 #HT2 #HX destruct -X /3/
35 | #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
36 elim (lift_inv_flat1 … HX) -HX #V #T #HV2 #HT2 #HX destruct -X /3/
40 lemma pr_subst_pr: ∀L,T1,T. L ⊢ T1 ⇒ T → ∀d,e,U. L ⊢ ↓[d,e] T ≡ U →
41 ∀T2. ↑[d,e] U ≡ T2 → L ⊢ T1 ⇒ T2.
42 #L #T1 #T #H elim H -H L T1 T
45 | #L #I #V1 #V2 #T1 #T2 #HV12 #HT12 #IHV12 #IHT12 #d #e #X2 #HX2 #X1 #HX1
46 elim (subst_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #H destruct -X2;
47 elim (lift_inv_bind1 … HX1) -HX1 #V4 #T4 #HV34 #HT34 #H destruct -X1;
48 @pr_bind /2 width=5/ @IHT12
49 | #L #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X2 #HX2 #X1 #HX1
50 elim (subst_inv_flat1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #H destruct -X2;
51 elim (lift_inv_flat1 … HX1) -HX1 #V4 #T4 #HV34 #HT34 #H destruct -X1;
53 | #L #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X2 #HX2 #X1 #HX1
54 elim (subst_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #H destruct -X2;
55 elim (lift_inv_bind1 … HX1) -HX1 #V4 #T4 #HV34 #HT34 #H destruct -X1;
56 @pr_beta /2 width=5/ @IHT12
57 | #L #K #V1 #V2 #V #i #HLK #HV12 #HV2 #IHV12 #d #e #U #HVU #U0 #HU0
58 lapply (lift_free … HU0 0 (i + 1 + e) ? ? ?) //
61 @pr_delta [4: // |1,2: skip |6: