Add match-syntax

In order to make the integration of general inductive types much easier, it would be in our best interest to add a general matching syntax. For now, the matching could be handled only by natural numbers, equality, true and false. The main challenge in this would be the exhaustiveness checking, to make sure the different branches of the matches can cover every case. Once this is done, the last obstacle to having a complete enough syntax for general inductives would be to add a termination-checker.