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