Alph:Type, P:(Alph*Prop). (n:. (l:Alph*. ||l|| < n P(l)) (l:Alph*. ||l|| = n P(l))) (l:Alph*. P(l))

1	1. Alph: Type 2. P: Alph*Prop 3. n:. (l:Alph*. ||l|| < n P(l)) (l:Alph*. ||l|| = n P(l)) 4. l: Alph* P(l)

About: