theorem T0 (α : Type) (x : α) (H: α → False) : False := by
  contradiction