Lemma isaprop_wma_inhab' X : (X -> iscontr X) -> isaprop X. Proof. intros f. apply isaprop_wma_inhab. intro x. apply isapropifcontr. apply (f x). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.