x:A. B(x)
Q
A
}
T}
Q
Q
b
x:A. B(x)
T Q
| Def | x:A. B(x) | [exists] | core | |
| Def | Dec(P) | [decidable] | core | |
| Def | Prop | [prop] | core | |
| Def | P Q | [or] | core | |
| Def | {T} | [guard] | core | |
| Def | SqStable(P) | [sq_stable] | core | |
| Def | True | [true] | core | |
| Def | A | [not] | core | |
| Def | {T} | [equivalence] | ||
| Def | S T | [subtype] | core | |
| Def | {T=} | [discrete_equality] | discrete jlc | |
| Def | P Q | [implies] | core | |
| Def | P Q | [iff] | core | |
| Def | b | [assert] | bool 1 | |
| Def | x:A. B(x) | [all] | core | |
| Def | P & Q | [and] | core | |
| Def | | [bool] | bool 1 | |
| Def | T | [squash] | core | |
| Def | P Q | [rev_implies] | core |
About:
 |  |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |  |