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