Verifying weight biased leftist heaps using dependent types