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