Proposition from_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 in p ; cbn in p. rewrite equal_subst in p. rewrite hyperdoctrine_pr1_subst in p. rewrite hyperdoctrine_pr2_subst in p. rewrite !var_tm_subst in p. rewrite hyperdoctrine_pair_pr1 in p. rewrite hyperdoctrine_pair_pr2 in p. 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.