lemma fquqa_refl: tri_reflexive … fquqa.
// qed.
-lemma fquqa_drop: ∀G,L,K,T,U,e.
- â\87©[e] L â\89¡ K â\86\92 â\87§[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.
+ â¬\87[m] L â\89¡ K â\86\92 â¬\86[0, m] T ≡ U → ⦃G, L, U⦄ ⊐⊐⸮ ⦃G, K, T⦄.
+#G #L #K #T #U #m #HLK #HTU elim (eq_or_gt m)
/3 width=5 by fqu_drop_lt, or_introl/ #H destruct
->(ldrop_inv_O2 … HLK) -L >(lift_inv_O2 … HTU) -T //
+>(drop_inv_O2 … HLK) -L >(lift_inv_O2 … HTU) -T //
qed.
(* Main properties **********************************************************)