t else f fi == InjCase(b ; t; f)
b:
, A:Type, p,q:A. if b p else q fi 
A| Who Cites ifthenelse? | |
| ifthenelse | Def if b t else f fi == InjCase(b ; t; f) |
|
Thm* b:, A:Type, p,q:A. if b p else q fi A |
| Syntax: | if b t else f fi | has structure: | ifthenelse(b; t; f) |
About:
 |  |
 |  |  |
 |  |