Actually leave the type implicit since that's what the text says

[holtzermann17]

The text said that the type should be left implicit, but the notation preserved the type. This fixes it.

The proof goes through as expected!

example : ∃ x, x + 2 = 8 :=
begin
  let a := 3 * 2,
  existsi a,
  reflexivity
end