T:Type. T 
Type| NOTE: | The "guard" operator, which is usually invisible, is used in some lemmas simply to guide matching heuristics, and has no semantic significance. |
| Who Cites guard? | |
| guard | Def {T} == T |
| Thm* T:Type. T Type |
| Syntax: | T | has structure: | guard(T) |
About:
 |  |  |  |