x:A. B(x)
Q
}
T
x:A. B(x)
b
Q
A Q
| Def | x:A. B(x) | [exists] | core | |
| Def | Discrete{T} | [discrete] | ||
| Def | P Q | [implies] | core | |
| Def | {T=} | [discrete_equality] | ||
| Def | S T | [subtype] | core | |
| Def | P & Q | [and] | core | |
| Def | True | [true] | core | |
| Def | Dec(P) | [decidable] | core | |
| Def | x:A. B(x) | [all] | core | |
| Def | b | [assert] | bool 1 | |
| Def | P Q | [iff] | core | |
| Def | | [bool] | bool 1 | |
| Def | A | [not] | core | |
| Def | P Q | [rev_implies] | core |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |
 |  |  |  |  |  |  |
 |