set T = elementary_tree 0 ;
thus tree (elementary_tree 0 ),(elementary_tree 0 ) = tree (2 |-> (elementary_tree 0 )) by FINSEQ_2:75
.= elementary_tree 2 by Th57 ; :: thesis: verum