Added support for induction tactic (works only for nonparameterized types insofar, requires eliminator for type)

We can now do proofs like these:
```Idris
ELIMTest.pluscommutes_proof = proof
  intros
  induction n
  compute
  rewrite (n_plus_O m)
  trivial
  intros
  compute
  rewrite (sym iht__0)
  rewrite (n_plus_S_m m t__0)
  trivial
```