l:Label. l 
Termx:Label. ts_fvar(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 tfvar? | |
| tfvar | Def l == tree_leaf(ts_fvar(l)) |
| Thm* l:Label. l Term | |
| ts_fvar | Def ts_fvar(x) == inr(inr(inr(inl(x)))) |
| Thm* x:Label. ts_fvar(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: | tfvar(l) |
About:
 |  |  |  |  |  |