Show $\vdash P(a) \to \forall x(P(x) \lor \lnot(x=a))$ using natural deduction Can somebody help me with this question?
The question is to show
$$\vdash P(a) \to \forall x(P(x) \lor \lnot(x=a))$$ 
using natural deduction.
Here is my attempt: 

I think I am going half-way through the question but I can't reach the conclusion.
My proof is right until line 8, but when I want to use the "implication introduction rule" my proof goes wrong.
Edit: I am using the online proof checker from https://proofs.openlogicproject.org/
 A: [
$\quad$P(a)$\quad${Entering a fantasy}
$\quad$[
$\quad\quad$$x=a$$\quad${Entering a fantasy}
$\quad\quad$P(a)$\quad${Bringing inside fantasy}
$\quad\quad$P(x)$\quad${Substitution with $x=a$}
$\quad$]
$\quad$$x=a$ implies P(x)$\quad${Fantasy rule}
$\quad$!! $x=a$ implies P(x)$\quad${Adding double negative}
$\quad$! $x=a$ or P(x)$\quad${Switcheroo rule}
]
P(a) implies !$x=a$ or P(x)$\quad${Fantasy rule}
P(a) implies ALLx: !$x=a$ or P(x)$\quad${x is a free variable}
QED
By the way I have used '!' for "not"
I have used [] to enter and exit fantasies.
All the logical terminology is from the book Godel Escher Bach
A: Using the DC Proof 2.0 proof checker ('|' is the OR-operator)

A: The following proof uses the proof checker used by the OP and Adam's hint on Philosophy SE: 

The part that may offer some confusion is the equality elimination (=E) on line 9. What it does is substitutes $a$ for $b$ in $\lnot Pb$ on line 6 to get $\lnot Pa$ on line 9.
Consider the attempt made by the OP:

The reason there is an issue with line 9 is because the subproof is between lines 2 and 8, not between lines 1 and 8.  Starting with the assumption on line 2 one is not able to discharge that assumption with any available rule.  One has to discharge the assumption on line 2 and then one can introduce the conditional.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/
