{u v u' v' : V@{U' U}} : (u = u') * (v = v') -> V_pair u v = V_pair u' v'. Proof. intros (H1, H2). apply setext'. split. + apply Bool_ind. * apply tr; exists true. assumption. * apply tr; exists false; assumption. + apply Bool_ind. * apply tr; exists true; assumption. * apply tr; exists false; assumption. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.