d:Decl, a:(
d). kind(a) 
LabelM:sm{i:l}(), a:M.action. kind(a) Label & kind(a) PatternA:Type, B:(A
Type), p:(a:A
B(a)). 1of(p) A| Who Cites kind? | |
| kind | Def kind(a) == 1of(a) |
| Thm* d:Decl, a:(d). kind(a) Label | |
|
Thm* M:sm{i:l}(), a:M.action. kind(a) Label & kind(a) Pattern | |
| pi1 | Def 1of(t) == t.1 |
| Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p) A |
About:
 |  |  |  |  |  |  |  |