l:Label. trace(l) 
Termx:Label. ts_trace(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 ttrace? | |
| ttrace | Def trace(l) == tree_leaf(ts_trace(l)) |
| Thm* l:Label. trace(l) Term | |
| ts_trace | Def ts_trace(x) == inr(inr(inr(inr(x)))) |
| Thm* x:Label. ts_trace(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: | trace(l) | has structure: | ttrace(l) |
About:
 |  |  |  |  |  |