take <*> D ; :: thesis: <*> D is empty
thus <*> D is empty ; :: thesis: verum