forall {A B : Type} (R : A -> B -> HProp) (bitot_R : bitotal R) (h : SPushout R -> V), set (h o (spushl R)) = set (h o (spushr R)).
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.