Don't use types for logic, then you have already escaped. Of course, if you prefer living in a prison, that's up to you. If you want equivalence, use an equival

Don't use types for logic, then you have already escaped. Of course, if you prefer living in a prison, that's up to you. If you want equivalence, use an equivalence relation.