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