remove EqDec requirement for hlist_nth_hlist_app

- transparent proofs make all the difference.