T:Type, x:Atom. ptn_atom(x) 
ptn_con(T)x:Atom. ptn_atom(x) Patternx:Atom. ptn_atom(x) Label| Who Cites ptn atom? | |
| ptn_atom | Def ptn_atom(x) == inl(x) |
| Thm* T:Type, x:Atom. ptn_atom(x) ptn_con(T) | |
|
Thm* x:Atom. ptn_atom(x) Pattern | |
|
Thm* x:Atom. ptn_atom(x) Label |
About:
 |  |  |  |  |  |