#check True → (∃ a : Nat, a = a)
-- True → ∃ a, a = a : Prop

#check True → (∃ b : Nat, b = b)
-- True → ∃ b, b = b : Prop