+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/relocation/drops_weight.ma".
+include "basic_2/s_computation/fqup_weight.ma".
+include "basic_2/s_computation/fqus_fqup.ma".
+include "basic_2/static/frees.ma".
+
+corec lemma sle_refl: ∀f. f ⊆ f.
+#f cases (pn_split f) * #g #H
+[ @(sle_push … H H) | @(sle_next … H H) ] -H //
+qed.
+
+lemma sle_inv_tl1: ∀f1,f2. ⫱f1 ⊆ f2 → f1 ⊆ ⫯f2.
+#f1 elim (pn_split f1) * #g #H destruct
+/2 width=5 by sle_next, sle_weak/
+qed-.
+
+axiom sor_tls: ∀f1,f2,f. f1 ⋓ f2 ≡ f →
+ ∀n. ⫱*[n]f1 ⋓ ⫱*[n]f2 ≡ ⫱*[n]f.
+
+axiom sor_sle1: ∀f1,f2,f. f1 ⋓ f2 ≡ f →
+ ∀g. g ⊆ f1 → g ⊆ f.
+
+axiom sor_sle2: ∀f1,f2,f. f1 ⋓ f2 ≡ f →
+ ∀g. g ⊆ f2 → g ⊆ f.
+
+lemma fqus_inv_refl_atom3: ∀I,G,L,X. ⦃G, L, ⓪{I}⦄ ⊐* ⦃G, L, X⦄ → ⓪{I} = X.
+#I #G #L #X #H elim (fqus_inv_fqup … H) -H [2: * // ]
+#H lapply (fqup_fwd_fw … H) -H
+#H elim (lt_le_false … H) -H /2 width=1 by monotonic_le_plus_r/
+qed-.
+
+axiom drops_T_isuni_inv_refl: ∀n,L. ⬇*[n] L ≡ L → n = 0.
+
+axiom fqus_split_fqu: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ →
+ (∧∧ G1 = G2 & L1 = L2 & T1 = T2) ∨
+ ∃∃G,L,T. ⦃G1, L1, T1⦄ ⊐ ⦃G, L, T⦄ & ⦃G, L, T⦄ ⊐* ⦃G2, L2, T2⦄.
+
+axiom fqus_inv_atom1: ∀I,G1,G2,L2,T2. ⦃G1, ⋆, ⓪{I}⦄ ⊐* ⦃G2, L2, T2⦄ →
+ ∧∧ G1 = G2 & ⋆ = L2 & ⓪{I} = T2.
+
+axiom fqus_inv_sort1: ∀G1,G2,L1,L2,T2,s. ⦃G1, L1, ⋆s⦄ ⊐* ⦃G2, L2, T2⦄ →
+ ∧∧ G1 = G2 & L1 = L2 & ⋆s = T2.
+
+axiom fqus_inv_zero1: ∀I,G1,G2,L1,L2,V1,T2. ⦃G1, L1.ⓑ{I}V1, #0⦄ ⊐* ⦃G2, L2, T2⦄ →
+ (∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & #0 = T2) ∨ ⦃G1, L1, V1⦄ ⊐* ⦃G2, L2, T2⦄.
+
+axiom fqus_inv_lref1: ∀I,G1,G2,L1,L2,V1,T2,i. ⦃G1, L1.ⓑ{I}V1, #⫯i⦄ ⊐* ⦃G2, L2, T2⦄ →
+ (∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & #(⫯i) = T2) ∨ ⦃G1, L1, #i⦄ ⊐* ⦃G2, L2, T2⦄.
+
+axiom fqus_inv_gref1: ∀G1,G2,L1,L2,T2,l. ⦃G1, L1, §l⦄ ⊐* ⦃G2, L2, T2⦄ →
+ ∧∧ G1 = G2 & L1 = L2 & §l = T2.
+
+axiom fqus_inv_bind1: ∀p,I,G1,G2,L1,L2,V1,T1,T2. ⦃G1, L1, ⓑ{p,I}V1.T1⦄ ⊐* ⦃G2, L2, T2⦄ →
+ ∨∨ ∧∧ G1 = G2 & L1 = L2 & ⓑ{p,I}V1.T1 = T2
+ | ⦃G1, L1, V1⦄ ⊐* ⦃G2, L2, T2⦄
+ | ⦃G1, L1.ⓑ{I}V1, T1⦄ ⊐* ⦃G2, L2, T2⦄.
+
+axiom fqus_inv_flat1: ∀I,G1,G2,L1,L2,V1,T1,T2. ⦃G1, L1, ⓕ{I}V1.T1⦄ ⊐* ⦃G2, L2, T2⦄ →
+ ∨∨ ∧∧ G1 = G2 & L1 = L2 & ⓕ{I}V1.T1 = T2
+ | ⦃G1, L1, V1⦄ ⊐* ⦃G2, L2, T2⦄
+ | ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄.
+
+(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
+
+lemma frees_drops_sle: ∀f1,G,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 →
+ ∀L2,T2. ⦃G, L1, T1⦄ ⊐* ⦃G, L2, T2⦄ →
+ ∀I,n. ⬇*[n] L1 ≡ L2.ⓑ{I}T2 →
+ ∃∃f2. L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 & f2 ⊆ ⫱*[⫯n] f1.
+#f1 #G #L1 #T1 #H elim H -f1 -L1 -T1
+[ #f1 #J #Hf1 #L2 #T2 #H12 #I #n #HL12
+ elim (fqus_inv_atom1 … H12) -H12 #H1 #H2 #H3 destruct
+ lapply (drops_fwd_lw … HL12) -HL12 #HL12
+ elim (lt_le_false … HL12) -HL12 //
+| #f1 #J #L1 #V1 #s #_ #_ #L2 #T2 #H12 #I #n #HL12
+ elim (fqus_inv_sort1 … H12) -H12 #H1 #H2 #H3 destruct
+ lapply (drops_fwd_lw … HL12) -HL12 #HL12
+ elim (lt_le_false … HL12) -HL12 //
+| #f1 #J #L1 #V1 #Hf1 #IH #L2 #T2 #H12
+ elim (fqus_inv_zero1 … H12) -H12 [ * | #H12 #I * ]
+ [ -IH -Hf1 #H1 #H2 #H3 #I #n #HL12 destruct
+ lapply (drops_fwd_lw … HL12) -HL12 #HL12
+ elim (lt_le_false … HL12) -HL12 //
+ | -IH -H12 #HL12 lapply (drops_fwd_isid … HL12 ?) -HL12 //
+ #H destruct /3 width=3 by sle_refl, ex2_intro/
+ | -Hf1 #n #HL12 lapply (drops_inv_drop1 … HL12) -HL12
+ #HL12 elim (IH … H12 … HL12) -IH -H12 -HL12 /3 width=3 by ex2_intro/
+ ]
+| #f1 #J #L1 #V1 #i #Hf1 #IH #L2 #T2 #H12
+ elim (fqus_inv_lref1 … H12) -H12 [ * | #H12 #I * ]
+ [ -IH -Hf1 #H1 #H2 #H3 #I #n #HL12 destruct
+ lapply (drops_fwd_lw … HL12) -HL12 #HL12
+ elim (lt_le_false … HL12) -HL12 //
+ | -IH #HL12 lapply (drops_fwd_isid … HL12 ?) -HL12 //
+ #H destruct <(fqus_inv_refl_atom3 … H12) -H12 /2 width=3 by sle_refl, ex2_intro/
+ | -Hf1 #I #HL12 lapply (drops_inv_drop1 … HL12) -HL12
+ #HL12 elim (IH … H12 … HL12) -IH -H12 -HL12 /3 width=3 by ex2_intro/
+ ]
+| #f1 #J #L1 #V1 #l #_ #_ #L2 #T2 #H12 #I #n #HL12
+ elim (fqus_inv_gref1 … H12) -H12 #H1 #H2 #H3 destruct
+ lapply (drops_fwd_lw … HL12) -HL12 #HL12
+ elim (lt_le_false … HL12) -HL12 //
+| #f1V #f1T #f1 #p #J #L1 #V #T #_ #_ #Hf1 #IHV #IHT #L2 #T2 #H12 #I #n #HL12
+ elim (fqus_inv_bind1 … H12) -H12 [ * |*: #H12 ]
+ [ -IHV -IHT -Hf1 #H1 #H2 #H3 destruct
+ lapply (drops_fwd_lw … HL12) -HL12 #HL12
+ elim (lt_le_false … HL12) -HL12 //
+ | -IHT elim (IHV … H12 … HL12) -IHV -H12 -HL12
+ /4 width=6 by sor_tls, sor_sle1, ex2_intro/
+ | -IHV elim (IHT … H12 I (⫯n)) -IHT -H12 /2 width=1 by drops_drop/ -HL12
+ <tls_xn /4 width=6 by ex2_intro, sor_tls, sor_sle2/
+ ]
+| #f1V #f1T #f1 #J #L1 #V #T #_ #_ #Hf1 #IHV #IHT #L2 #T2 #H12 #I #n #HL12
+ elim (fqus_inv_flat1 … H12) -H12 [ * |*: #H12 ]
+ [ -IHV -IHT -Hf1 #H1 #H2 #H3 destruct
+ lapply (drops_fwd_lw … HL12) -HL12 #HL12
+ elim (lt_le_false … HL12) -HL12 //
+ | -IHT elim (IHV … H12 … HL12) -IHV -H12 -HL12
+ /4 width=6 by sor_tls, sor_sle1, ex2_intro/
+ | -IHV elim (IHT … H12 … HL12) -IHT -H12 -HL12
+ /4 width=6 by ex2_intro, sor_tls, sor_sle2/
+ ]
+]
+qed-.