for i being Nat holds elementary_tree i = tree (i |-> (elementary_tree 0))