2 lines
60 B
Text
2 lines
60 B
Text
definition foo : empty → empty :=
|
|
empty.rec (λ e, empty)
|
definition foo : empty → empty :=
|
|
empty.rec (λ e, empty)
|