Proposition eq_in_exp_partial_setoid {Γ : ty H} {f g : tm Γ exp_partial_setoid} {Δ : form Γ} (p : Δ ⊢ exp_partial_setoid_is_function [ f ]) (q : Δ ⊢ exp_partial_setoid_eq [⟨ f , g ⟩]) : Δ ⊢ f ~ g. Proof. unfold partial_setoid_formula ; cbn. simplify. use conj_intro. - exact p. - 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.