b == if b
True else False fi
b:
. b 
Prop
; z. false)A,B:Type, x:A+B. isl(x) l) == 
i:
. i < ||l|| & x = l[i] TT:Type, x:T, l:T List. (x l) PropA,B:Type, x:A+B. isl(x) 
outl(x) A| Some definitions of interest. | |
| assert | Def b == if b True else False fi |
| Thm* b:. b Prop | |
| isl | Def isl(x) == InjCase(x; y. true; z. false) |
| Thm* A,B:Type, x:A+B. isl(x) | |
| l_member | Def (x l) == i:. i < ||l|| & x = l[i] T |
| Thm* T:Type, x:T, l:T List. (x l) Prop | |
| outl | Def outl(x) == InjCase(x; y. y; z. "???") |
| Thm* A,B:Type, x:A+B. isl(x) outl(x) A |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |
 |  |  |  |  |  |