Lemma decidable_ishinh {X} : decidable X → decidable(∥X∥). Proof. intros d. unfold decidable in *. induction d as [x|x']. - apply ii1. apply hinhpr. assumption. - apply ii2. intros p. apply (squash_to_prop p). + exact isapropempty. + exact x'. Defined.