x,y:Pattern. lbl_pr( < x, y > ) 
Patternx,y:Label. lbl_pr( < x, y > ) LabelT:Type, x:(T
T). ptn_pr(x) ptn_con(T)x,y:Pattern. ptn_pr( < x,y > ) Pattern| Who Cites lbl pair? | |
| lbl_pair | Def lbl_pr( < x, y > ) == ptn_pr( < x,y > ) |
| Thm* x,y:Pattern. lbl_pr( < x, y > ) Pattern | |
|
Thm* x,y:Label. lbl_pr( < x, y > ) Label | |
| ptn_pr | Def ptn_pr(x) == inr(inr(inr(x))) |
| Thm* T:Type, x:(TT). ptn_pr(x) ptn_con(T) | |
|
Thm* x,y:Pattern. ptn_pr( < x,y > ) Pattern |
| Syntax: | lbl_pr( < x, y > ) | has structure: | lbl_pair(x; y) |
About:
 |  |  |  |  |  |  |