f:Label. f 
Termx:Label. ts_op(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 topr? | |
| topr | Def f == tree_leaf(ts_op(f)) |
| Thm* f:Label. f Term | |
| ts_op | Def ts_op(x) == inr(inr(inl(x))) |
| Thm* x:Label. ts_op(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: | f | has structure: | topr(f) |
About:
 |  |  |  |  |  |