= y= y
x:A. B(x)
A
Q
Q
x:A. B(x) Q
| Def | A Term | [termof] | ||
| Def | Prop | [prop] | core | |
| Def | closed(t) | [term_closed] | ||
| Def | s(t) | [s] | ||
| Def | RepsTruth(L; Tr; tr) | [RepsTruth] | ||
| Def | False | [false] | core | |
| Def | A & B | [cand] | core | |
| Def | ReflectsProp(P; qP; Tr) | [ReflectsProp] | ||
| Def | x = y | [repst] | ||
| Def | x = y | [reps] | ||
| Def | x:A. B(x) | [all] | core | |
| Def | f(t) | [f] | ||
| Def | SUBX(t; e) | [subx] | ||
| Def | RespectsNot(Tr; L) | [RespectsNot] | ||
| Def | A | [not] | core | |
| Def | P & Q | [and] | core | |
| Def | P Q | [iff] | core | |
| Def | {T} | [guard] | core | |
| Def | P Q | [implies] | core | |
| Def | x:A. B(x) | [exists] | core | |
| Def | P Q | [rev_implies] | core |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |  |  |