-lemma fquqa_drop: ∀G,L,K,T,U,e.
- ⬇[e] L ≡ K → ⬆[0, e] T ≡ U → ⦃G, L, U⦄ ⊐⊐⸮ ⦃G, K, T⦄.
-#G #L #K #T #U #e #HLK #HTU elim (eq_or_gt e)
+lemma fquqa_drop: ∀G,L,K,T,U,m.
+ ⬇[m] L ≡ K → ⬆[0, m] T ≡ U → ⦃G, L, U⦄ ⊐⊐⸮ ⦃G, K, T⦄.
+#G #L #K #T #U #m #HLK #HTU elim (eq_or_gt m)