definition foo : empty → empty :=
empty.rec (λ e, empty)