setext' {A B : Type} (f : A -> V) (g : B -> V) (eq_img : equal_img f g) : set f = set g. Proof. pose (R := fun a b => Build_HProp (f a = g b)). pose (h := SPushout_rec R V f g (fun _ _ r => r)). exact (setext R eq_img h). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.