/4 width=1 by apply_basic_ge, (* 2x *) eq_f/
qed-.
-lemma flifts_basic_bind (p) (I) (V) (T) (d) (h): ↑[d,h](ⓑ{p,I}V.T) = ⓑ{p,I}(↑[d,h]V).(↑[↑d,h]T).
+lemma flifts_basic_bind (p) (I) (V) (T) (d) (h): ↑[d,h](ⓑ[p,I]V.T) = ⓑ[p,I](↑[d,h]V).(↑[↑d,h]T).
// qed.