Comment by solomonb

How does `refl` work if its not even dependently typed?