-lemma fqu_inv_eq: ∀G,L1,L2,T. ⦃G, L1, T⦄ ⊐ ⦃G, L2, T⦄ → |L1| = |L2| → ⊥.
-#G #L1 #L2 #T #H #H0 @(fqu_inv_eq_aux … H … H0) // (**) (* full auto fails *)
+lemma fqu_inv_eq: ∀b,G,L1,L2,T. ⦃G, L1, T⦄ ⊐[b] ⦃G, L2, T⦄ → |L1| = |L2| → ⊥.
+#b #G #L1 #L2 #T #H #H0 @(fqu_inv_eq_aux … H … H0) // (**) (* full auto fails *)