:: deftheorem defines TrivialInfiniteTree TREES_1:def 14 :
TrivialInfiniteTree = { (k |-> 0) where k is Nat : verum } ;