matita/matita/contribs/lambdadelta/basic_2/etc_new/fqu/fqu.etc

   1 (* Removed theorems *********************************************************)
   2
   3 include "basic_2/substitution/drop.ma".
   4
   5 | fqu_drop   : ∀G,L,K,T,U,k.
   6                ⬇[⫯k] L ≡ K → ⬆[0, ⫯k] T ≡ U → fqu G L U G K T
   7
   8 lemma fqu_drop_lt: ∀G,L,K,T,U,k. 0 < k →
   9                    ⬇[k] L ≡ K → ⬆[0, k] T ≡ U → ⦃G, L, U⦄ ⊐ ⦃G, K, T⦄.
  10 #G #L #K #T #U #k #Hm lapply (ylt_inv_O1 … Hm) -Hm
  11 #Hm <Hm -Hm /2 width=3 by fqu_drop/
  12 qed.
  13
  14 lemma fqu_lref_S_lt: ∀I,G,L,V,i. yinj 0 < i → ⦃G, L.ⓑ{I}V, #i⦄ ⊐ ⦃G, L, #(⫰i)⦄.
  15 /4 width=3 by drop_drop, lift_lref_pred, fqu_drop/
  16 qed.