DEFINITION clear_gen_sort()
TYPE =
∀
x:
C
.
∀
n:
nat
.(
clear
(
CSort
n) x)
→
∀
P:
Prop
.P
BODY =
Show proof