proposition: Lemma decidable_ishinh {X} : decidable X → decidable(∥X∥).
proof: 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.
imports: UniMath.Foundations.PartD