take <*> D ; :: thesis: <*> D is one-to-one
thus <*> D is one-to-one ; :: thesis: verum