[dependenttypes]

> where you should be able to more cheaply run a preimage attack against two 64bit hash functions than one 128bit hash function.

Try doing that in my example.

[freemint]

Your hash functions are contrustructed in a way such that the concatenation has the security properties of a 128 bit hash function (because your construction is equivalent md5). I am not sure that results holds for all concatenations of hash functions. Or for SHA concatenations.

I appreciate you making me think deeper about hash functions. Nice construction.