Proposition exp_partial_setoid_im_exists {Γ : ty H} {Δ : form Γ} {f : tm Γ (ℙ (X ×h Y))} (p : Δ ⊢ exp_partial_setoid_is_function [ f ]) {x : tm Γ X} (q : Δ ⊢ x ~ x) : Δ ⊢ (∃h (⟨ x [ π₁ (tm_var _) ]tm , π₂ (tm_var _) ⟩ ∈ (f [ π₁ (tm_var _) ]tm))). Proof. unfold exp_partial_setoid_is_function in p. rewrite !conj_subst in p. pose proof (r := conj_elim_right (conj_elim_right (conj_elim_right (conj_elim_right p)))). clear p. unfold exp_partial_setoid_im_exists_law in r. rewrite !forall_subst in r. pose (r' := forall_elim r x). refine (weaken_cut r' _). simplify_form. rewrite partial_setoid_subst. simplify. use (impl_elim _ (weaken_right (hyperdoctrine_hyp _) _)). use weaken_left. exact q. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.Tripos. Require Import UniMath.CategoryTheory.Hyperdoctrines.GenericPredicate. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERs. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERMorphisms.