Reducibility properties + normalization

[Ayertienna]

We need to formalize strong normalization using Tait's method. This will be done in 3 steps:

1. Define reducibility for simple lambda calculus, prove the required properties etc
2. Extend to box
3. Extend to box & diamond

[Ayertienna]

This was started (work on part 1 only for now, not yet finished - problems with good strong_norm definition)

[Ayertienna]

part 1 is now finished, part 2 was started
For the sake of satisfying my curiosity I will try to write an alternative version of this - using label-free language (current version uses labeled - and in the de Bruijn flavor - so a rewrite at some point is inevitable)

[Ayertienna]

still work in progress for 1&2 together (but in LF case, so it's a cheaty cheat)