// qed.
lemma fquqa_drop: ∀G,L,K,T,U,e.
- ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → ⦃G, L, U⦄ ⊃⊃⸮ ⦃G, K, T⦄.
+ ⇩[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)
/3 width=5 by fqu_drop_lt, or_introl/ #H destruct
>(ldrop_inv_O2 … HLK) -L >(lift_inv_O2 … HTU) -T //