fact: Definition sig_of_sum A B (x : A + B) : { b : Bool & if b then A else B } := (_; match x as s return (if match s with | inl _ => true | inr _ => false end then A else B) with | inl a => a | inr b => b end).
imports: HoTT.Basics Types.Empty Types.Unit Types.Prod Types.Sigma Types.Bool Types.Forall