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