take <*(1. R)*> ; :: thesis: ( <*(1. R)*> is quadratic & not <*(1. R)*> is trivial )
thus ( <*(1. R)*> is quadratic & not <*(1. R)*> is trivial ) ; :: thesis: verum