| Who Cites is leaf? |
|
is_leaf | Def is_leaf(t) == Case(t) Case tree_leaf(l) => true Default => false |
| | Thm* E:Type, t:Tree(E). is_leaf(t)  |
|
case_default | Def Default => body(value,value) == body |
|
case_tree_leaf | Def Case tree_leaf(x) => body(x) cont(x1,z)
Def == InjCase(x1; x2. body(x2); _. cont(z,z)) |
|
case | Def Case(value) body == body(value,value) |