(* *)
(**************************************************************************)
+include "ground/lib/arith_2a.ma".
+include "ground/ynat/ynat_minus_sn.ma".
include "basic_2A/substitution/drop_drop.ma".
include "basic_2A/multiple/frees.ma".
| -IH /3 width=5 by frees_inv_gref, or_intror/
| #a #I #W #U #Hx #l #i destruct
elim (IH L W … l i) [1,3: /3 width=1 by frees_bind_sn, or_introl/ ] #HnW
- elim (IH (L.â\93\91{I}W) U â\80¦ (⫯l) (i+1)) -IH [1,3: /3 width=1 by frees_bind_dx, or_introl/ ] #HnU
+ elim (IH (L.â\93\91{I}W) U â\80¦ (â\86\91l) (i+1)) -IH [1,3: /3 width=1 by frees_bind_dx, or_introl/ ] #HnU
@or_intror #H elim (frees_inv_bind … H) -H /2 width=1 by/
| #I #W #U #Hx #l #i destruct
elim (IH L W … l i) [1,3: /3 width=1 by frees_flat_sn, or_introl/ ] #HnW
]
qed-.
+alias symbol "UpArrow" (instance 2) = "ynat successor".
+alias symbol "minus" (instance 6) = "natural minus".
+alias symbol "minus" (instance 5) = "natural minus".
+alias symbol "RDrop" (instance 9) = "basic slicing (local environment) lget".
lemma frees_S: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[yinj l]⦃U⦄ → ∀I,K,W. ⬇[l] L ≡ K.ⓑ{I}W →
- (K â\8a¢ i-l-1 ϵ ð\9d\90\85*[0]â¦\83Wâ¦\84 â\86\92 â\8a¥) â\86\92 L â\8a¢ i ϵ ð\9d\90\85*[⫯l]⦃U⦄.
+ (K â\8a¢ i-l-1 ϵ ð\9d\90\85*[0]â¦\83Wâ¦\84 â\86\92 â\8a¥) â\86\92 L â\8a¢ i ϵ ð\9d\90\85*[â\86\91l]⦃U⦄.
#L #U #l #i #H elim (frees_inv … H) -H /3 width=2 by frees_eq/
* #I #K #W #j #Hlj #Hji #HnU #HLK #HW #I0 #K0 #W0 #HLK0 #HnW0
lapply (yle_inv_inj … Hlj) -Hlj #Hlj
lemma frees_inv_lift_ge: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ →
∀K,s,l0,m0. ⬇[s, l0, m0] L ≡ K →
∀T. ⬆[l0, m0] T ≡ U → l0 + m0 ≤ i →
- K ⊢ i-m0 ϵ𝐅*[l-yinj m0]⦃T⦄.
+ K ⊢ i-m0 ϵ𝐅*[l-m0]⦃T⦄.
#L #U #l #i #H elim H -L -U -l -i
[ #L #U #l #i #HnU #K #s #l0 #m0 #HLK #T #HTU #Hlm0i -L -s
elim (le_inv_plus_l … Hlm0i) -Hlm0i #Hl0im0 #Hm0i @frees_eq #X #HXT -K