-| fqu_lref_O : ∀I,G,L,V. fqu b G (L.ⓑ{I}V) (#0) G L V
-| fqu_pair_sn: ∀I,G,L,V,T. fqu b G L (②{I}V.T) G L V
-| fqu_bind_dx: ∀p,I,G,L,V,T. fqu b G L (ⓑ{p,I}V.T) G (L.ⓑ{I}V) T
-| fqu_clear : ∀p,I,G,L,V,T. b = Ⓕ → fqu b G L (ⓑ{p,I}V.T) G (L.ⓧ) T
-| fqu_flat_dx: ∀I,G,L,V,T. fqu b G L (ⓕ{I}V.T) G L T
-| fqu_drop : â\88\80I,G,L,T,U. â¬\86*[1] T â\89\98 U â\86\92 fqu b G (L.â\93\98{I}) U G L T
+| fqu_lref_O : ∀I,G,L,V. fqu b G (L.ⓑ[I]V) (#0) G L V
+| fqu_pair_sn: ∀I,G,L,V,T. fqu b G L (②[I]V.T) G L V
+| fqu_bind_dx: ∀p,I,G,L,V,T. b = Ⓣ → fqu b G L (ⓑ[p,I]V.T) G (L.ⓑ[I]V) T
+| fqu_clear : ∀p,I,G,L,V,T. b = Ⓕ → fqu b G L (ⓑ[p,I]V.T) G (L.ⓧ) T
+| fqu_flat_dx: ∀I,G,L,V,T. fqu b G L (ⓕ[I]V.T) G L T
+| fqu_drop : â\88\80I,G,L,T,U. â\87§[1] T â\89\98 U â\86\92 fqu b G (L.â\93\98[I]) U G L T