Proposition eq_in_eq_partial_setoid {Γ X : ty H} {t₁ t₂ : tm Γ (eq_partial_setoid X)} {Δ : form Γ} (p : Δ ⊢ t₁ ≡ t₂) : Δ ⊢ t₁ ~ t₂. Proof. unfold partial_setoid_formula ; cbn. simplify. exact p. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine.