Clean-up Syntax.agda
Added bisimilarity for normal forms.

Sadly, the proofs using this are not terminating.