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