| with x0
1 || not (P(x0) or not P(x0))	: assumption
2 ||| P(x0)										: assumption
3 ||| P(x0) or not P(x0)			: or intro1 2
4 ||| _|_											: not elim 1,3
5 || not P(x0)								: not intro 2-4
6 || P(x0) or not P(x0)				: or intro2 5
7 || _|_											: not elim 6,1
8 | P(x0) or not P(x0)				: PBC 1-7
9 A.x(P(x) or not P(x))				: A.x/x0 intro 1-8