totality020.idr:4:5:bug _ _ Refl is a valid case