== {l:(A List)| 
(0 < 
||l||) }
A:Type. A List 
Type
0 ; a.as' ||as'||+1 (recursive)A:Type, l:A List. ||l|| 
j == if i < j true ; false fii,j:. (i < j) 
b == if b True else False fib:. b Prop| Who Cites listp? | |
| listp | Def A List == {l:(A List)| (0 < ||l||) } |
| Thm* A:Type. A List Type | |
| length | Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive) |
| Thm* A:Type, l:A List. ||l|| | |
| Thm* ||nil|| | |
| lt_int | Def i < j == if i < j true ; false fi |
| Thm* i,j:. (i < j) | |
| assert | Def b == if b True else False fi |
| Thm* b:. b Prop |
| Syntax: | A List | has structure: | listp(A) |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |  |
 |  |  |  |  |  |  |  |