Proposition partial_setoid_subst {H : first_order_hyperdoctrine} {X : partial_setoid H} {Γ Γ' : ty H} (s : tm Γ Γ') (x y : tm Γ' X) : (x ~ y)[ s ] = (x [ s ]tm ~ y [ s ]tm). Proof. unfold partial_setoid_formula. simplify. apply idpath. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine.