proposition: Corollary subtypePath {A : UU} {B : A -> UU} (is : isPredicate B) {s s' : total2 (λ x, B x)} : pr1 s = pr1 s' -> s = s'.
proof: Proof. intros e. apply (total2_paths_f e). apply is. Defined.
imports: UniMath.Foundations.PartA