Lemma horelim ( A B : UU ) ( P : hProp ) : ( ishinh_UU A -> P ) × ( ishinh_UU B -> P ) -> A ∨ B -> P. Proof. intros p q. simpl in q. apply q. intro u. destruct u as [ u | v ]. - apply ( pr1 p ). intro Q. intro H. apply H. assumption. - apply ( pr2 p ). intro Q. intro H. apply H. assumption. Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Algebra.Monoids.