make injection do the right thing for /\

- There is possibly a better way to do this by
  exposing the conjunctions (possibly as dependent sums)
  and then reflecting the destruction of this.