Prove PER for per_ctx_env

[Ailrun]

Closes #61

[HuStmpHrrr]

Let's follow a bit closer to Agda's module structure and bring some hierarchy here as well. Unlike OCaml, Coq knows folders so there is no reason to keep files in a flap structure and use longer filenames to distinguish what they are for.

[Ailrun]

Sure, like PER directory that contains Lemmas and Definition, and PER module itself reexports them?

[HuStmpHrrr]

something along the line, as long as it makes the code easier to browse.

[Ailrun]

Let's do that refactoring in a different PR.