- updated equivalence on referred entries: it nust be degree-based

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc_new / fqu / fqu.etc

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/fqu/fqu.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/fqu/fqu.etc
deleted file mode 100644 (file)
index b5066d0..0000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/fqu/fqu.etc
+++ /dev/null
@@ -1,16 +0,0 @@
-(* 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.