proposition: Lemma horelim ( A B : UU ) ( P : hProp ) : ( ishinh_UU A -> P ) × ( ishinh_UU B -> P ) -> A ∨ B -> P.
proof: 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.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.NaturalNumbers UniMath.Algebra.RigsAndRings UniMath.Algebra.Domains_and_Fields UniMath.NumberSystems.Integers UniMath.Algebra.Monoids