set T = elementary_tree 0;
thus ^ (elementary_tree 0) = tree (1 |-> (elementary_tree 0)) by FINSEQ_2:73
.= elementary_tree 1 by Th57 ; :: thesis: verum