7.3 Inductively Defined Propositions

The problematic sentence is "Keep in mind that the notation ∃ x : α, p is syntactic sugar for [Exists] (fun x : α => p)."  I think that this should be "Keep in mind that the notation ∃ x : α, p x is syntactic sugar for [Exists] (fun x : α => p x)." like in 4.4 instead.
