Thm* V,T:Type{i}. Grammar(V;T) Type{i'}
Thm* T:Type. (T List) Type
Thm* A:Type, l:A*. ||l||
Thm* ||nil||
Thm* i,j:. i > j Prop
About: