[dependenttypes]

I am sure that I saw this exact message on HN before. Did you copy it from someone else or did you repost your own post?

[sooheon]

I wrote it out ad hoc, I don’t doubt that something similar has been written before though.