[일반] 형식 증명 같은 거 필요없는 거지??

[익명(218.232)]

집합론 책을 Coq로 옮기려고 해봤는데, 너무 어렵다.

Type(i) ≤ Prop이 성립하지 않기 때문에,

존재성 공리로부터 공집합을 얻어낼 수 없는 것 같은데,

어떻게 해결해야 됨??

sort인 Set은 쓰기 싫음 ...