Proposition eq_in_prod_partial_setoid_r {Γ : ty H} {t₁ t₂ : tm Γ prod_partial_setoid} {Δ : form Γ} (p : Δ ⊢ t₁ ~ t₂) : Δ ⊢ π₂ t₁ ~ π₂ t₂. Proof. refine (hyperdoctrine_cut p _). unfold partial_setoid_formula ; cbn ; unfold prod_per_data. simplify_form. rewrite !partial_setoid_subst. simplify. use weaken_right. apply hyperdoctrine_hyp. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine.