avoid vacous type variable, due to "potentially redundant" shyps in Thm.unconstrainT;