Lemma isaprop_wma_inhab X : (X -> isaprop X) -> isaprop X. Proof. intros f. apply invproofirrelevance. intros x y. apply (f x). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.