Short proof.
Remove redundant paren.
Update about pal.
Update subseq.
Update about pal.
Resolve some optional problems.
Update about pal.
Update about pal.
Add proposition about p_provability.
Add extra lemmas of list.