fun :: rforall a. {v:a | True} -> {v:Int | v == 0}
fun = \x -> 0