(* Removed theorems *********************************************************)

include "basic_2/substitution/drop.ma".

| fqu_drop   : ∀G,L,K,T,U,k.
               ⬇[⫯k] L ≡ K → ⬆[0, ⫯k] T ≡ U → fqu G L U G K T

lemma fqu_drop_lt: ∀G,L,K,T,U,k. 0 < k →
                   ⬇[k] L ≡ K → ⬆[0, k] T ≡ U → ⦃G, L, U⦄ ⊐ ⦃G, K, T⦄.
#G #L #K #T #U #k #Hm lapply (ylt_inv_O1 … Hm) -Hm
#Hm <Hm -Hm /2 width=3 by fqu_drop/
qed.

lemma fqu_lref_S_lt: ∀I,G,L,V,i. yinj 0 < i → ⦃G, L.ⓑ{I}V, #i⦄ ⊐ ⦃G, L, #(⫰i)⦄.
/4 width=3 by drop_drop, lift_lref_pred, fqu_drop/
qed.