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