fixing RType and porting Ext

- Removed typ_of_apply
- Removed instantiate_typ
- Renamed typ_cast to type_cast
- Renamed typ_eqb to type_eqb
- Renamed funcAs to symAs
- In Lambda
  - Implement type_of_apply using tvArr
add semi-decidable equality to RSym + examples

- Added semi-decidable equality to RSym
- Porting examples to work with the new extendable branch
- Started refactoring the mtac example (still a ways from
  being correct). I need to figure out a litle bit about
  the specification.
  - Also, note that McBride showed how to define unification
    using well-founded recursion.