fixed PlusZRightNeutral proof
added typechecking tests for the proofs about natural numbers
Fixed bug on variable substitution