proposition: Lemma weq_subtypes_iff {X : UU} {S T : X -> UU} (HS : isPredicate S) (HT : isPredicate T) (HST : ∏ x, S x <-> T x) : (∑ x, S x) ≃ (∑ x, T x).
proof: Proof. apply (weq_subtypes' (idweq X)); assumption. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics