bs ; a.as' [a / (as' @ bs)] (recursive)
T:Type, as,bs:T List. (as @ bs) 
T List
B == 
B < Ai,j:
. (ij) Prop 0 ; a.as' ||as'||+1 (recursive)A:Type, l:A List. ||l|| | Some definitions of interest. | |
| append | Def as @ bs == Case of as; nil bs ; a.as' [a / (as' @ bs)] (recursive) |
| Thm* T:Type, as,bs:T List. (as @ bs) T List | |
| le | Def AB == B < A |
| Thm* i,j:. (ij) Prop | |
| length | Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive) |
| Thm* A:Type, l:A List. ||l|| | |
| Thm* ||nil|| |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |  |  |