Splitted up languages in multiple files
Added an untyped lambda calculus and rename all language records to `language`.
Added some helper module.
Fixed substitution.
Added theorem e₁ ⇒ₜ e₂ → erase e₁ ⇒ᵤ erase e and proofed it for the untyped and typed lambda calculus.