Finish Realizability for PER

[Ailrun]

Resolves #35

[HuStmpHrrr]

There should also be some clean up PRs. For example, per_nat_then_per_top should be placed elsewhere. If you feel that you are on fire, you could also swallow Antoine's cake if you want to @Ailrun .

[Ailrun]

@HuStmpHrrr Why do you think so? They are all in the similar spirit, aren't they?

FYI, in Agda proof, they are merged together into a single mutual proof (with a more complex termination order)

[HuStmpHrrr]

at least this lemma and var_per_bot should live in the same file.

[Ailrun]

per_..._then_per_... things are about the lattice structure of PERs given here, and var_per_bot is a different from them, at least from my point of view.