l:Label. l 
Termx:Label. ts_var(x) ts()E,T:Type, x:E. tree_leaf(x) tree_con(E;T)E:Type, x:E. tree_leaf(x) Tree(E)| Who Cites tvar? | |
| tvar | Def l == tree_leaf(ts_var(l)) |
| Thm* l:Label. l Term | |
| ts_var | Def ts_var(x) == inl(x) |
| Thm* x:Label. ts_var(x) ts() | |
| tree_leaf | Def tree_leaf(x) == inl(x) |
| Thm* E,T:Type, x:E. tree_leaf(x) tree_con(E;T) | |
|
Thm* E:Type, x:E. tree_leaf(x) Tree(E) |
| Syntax: | l | has structure: | tvar(l) |
About:
 |  |  |  |  |