let x be Element of (FreeUnivAlgNSG (f,D)); :: thesis: x is DecoratedTree-like
thus x is DecoratedTree-like ; :: thesis: verum