theory B
  imports Bot
begin

lift_definition index_flip_subspace :: "int t \<Rightarrow> int t" is
  "undefined :: int \<Rightarrow> int"
  by simp

end