fact: Definition is_inl_and {A B} (P : A -> Type@{p}) : A + B -> Type@{p} := fun x => match x with inl a => P a | inr _ => Empty end.
imports: HoTT.Basics Types.Empty Types.Unit Types.Prod Types.Sigma Types.Bool Types.Forall