Allows induction on more complicated data types 

Works with all types that have eliminators now.
Still beta-ish as not thorough testing has been done, eliminators still need to be fixed for some data types namely those with implicit arguments.

Example proof:

```Idris
vlength : Vect n a -> Nat
vlength []        = 0
vlength (_ :: xs) = S (vlength xs)

vect_is_length_indexed : {v : Vect n a} -> n = vlength v
vect_is_length_indexed = ?p_vect_is_length_indexed

---------- Proofs ----------

p_vect_is_length_indexed = proof
  intros
  induction v
  trivial
  intros
  compute
  rewrite ihxs
  trivial
```