>I would like my month spent on transitivity of subclassing back :( Oh God, that gave me flashbacks. I've done at least one transitivity of subtyping proof wh

>I would like my month spent on transitivity of subclassing back :( Oh God, that gave me flashbacks. I've done at least one transitivity of subtyping proof where I actually got the right theorem, then found later in the module that I had to rewrite the whole thing with a graph-theory library supplying some theorems about DAGs/finite posets. It's horrible, and that piece of work still isn't done!