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 "Basic_2/unfold/tpss_lift.ma".
16 include "Basic_2/unfold/delift.ma".
18 (* DELIFT ON TERMS **********************************************************)
20 (* Advanced forward lemmas **************************************************)
22 lemma delift_fwd_lref1_lt: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 → i < d → U2 = #i.
23 #L #U2 #i #d #e * #U #HU #HU2 #Hid
24 elim (tpss_inv_lref1 … HU) -HU
25 [ #H destruct >(lift_inv_lref2_lt … HU2) //
27 lapply (lt_to_le_to_lt … Hid Hdi) -Hid -Hdi #Hi
28 elim (lt_refl_false … Hi)
32 lemma delift_fwd_lref1_be: ∀L,U2,d,e,i. L ⊢ #i [d, e] ≡ U2 →
34 ∃∃K,V1,V2. ⇩[0, i] L ≡ K. ⓓV1 &
35 K ⊢ V1 [0, d + e - i - 1] ≡ V2 &
37 #L #U2 #d #e #i * #U #HU #HU2 #Hdi #Hide
38 elim (tpss_inv_lref1 … HU) -HU
39 [ #H destruct elim (lift_inv_lref2_be … HU2 ? ?) //
40 | * #K #V1 #V #_ #_ #HLK #HV1 #HVU
41 elim (lift_div_be … HVU … HU2 ? ?) -U // /2 width=1/ /3 width=6/
45 lemma delift_fwd_lref1_ge: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 →
46 d + e ≤ i → U2 = #(i - e).
47 #L #U2 #i #d #e * #U #HU #HU2 #Hdei
48 elim (tpss_inv_lref1 … HU) -HU
49 [ #H destruct >(lift_inv_lref2_ge … HU2) //
50 | * #K #V1 #V2 #_ #Hide
51 lapply (lt_to_le_to_lt … Hide Hdei) -Hide -Hdei #Hi
52 elim (lt_refl_false … Hi)