list xs == Case of xs; nil 
False ; x.ys x = a A 
a list ys
Def (recursive)
A:Type, a:A, xs:A List. (a list xs) Prop T }T:Type, a:T. {a:T} Type
T == x:S. x T| Some definitions of interest. | |
| sfa_doc_inlist | list xs == Case of xs; nil False ; x.ys x = a A a list ys
Def (recursive) |
| A:Type, a:A, xs:A List. (a list xs) Prop | |
| singleton | T } |
| T:Type, a:T. {a:T} Type | |
| subtype | T == x:S. x T |
About:
 |  |  |
 |  |  |  |  |  |  |  |  |
 |