E:Type, t:Tree(E). right_child(t) 
Tree(E)| No other cites to report in MarkB_generic | |
| right_child | Def right_child(t) == Case(t) Case x;y = > y Default = > t |
| Thm* E:Type, t:Tree(E). right_child(t) Tree(E) | |
| case_default | Def Default = > body(value,value) == body |
| case_node | Def Case x;y = > body(x;y) cont(x1,z) == InjCase(x1; _. cont(z,z); x2. x2/x3,x2@0. body(x3;x2@0)) |
| case | Def Case(value) body == body(value,value) |
About:
 |  |
 |  |  |  |  |