| Who Cites left child? |
|
left_child | Def left_child(t) == Case(t) Case x;y => x Default => t |
|
| Thm* E:Type, t:Tree(E). left_child(t) Tree(E) |
|
case_default | Def Default => body(value,value) == body |
|
case_node | Def Case x;y => body(x;y) cont(x1,z)
Def == InjCase(x1; _. cont(z,z); x2. x2/x3,x2@0. body(x3;x2@0)) |
|
case | Def Case(value) body == body(value,value) |