Delete minus1Trunc.v, close #434

Why the switch from "is monomorphism" to "is embedding"?