/sci/ - Science & Math

>>10855653
It's the same rules
(pic related taken from
https://en.wikipedia.org/wiki/Natural_deduction#First_and_higher-order_extensions
)
except that my calculus is "proof relevant" (the proofs are mathematical objects in themselves and you state proof and propositions) while the one in your pic just forms the propositions.

In any case, do you logically understand why your theorem is evident?
PS the pic you posted has not \exists introduction, so with that alone you naturally won't get far in building up your proposition.
State your sheet with \exist introduction and then try to build it up assuming x=x and that you can set y:=x.