Proposition hyperdoctrine_eq_elim_help_con {H : first_order_hyperdoctrine} {Γ A : ty H} (φ : form (Γ ×h (A ×h A))) (p : ⊤ ⊢ φ [ ⟨ π₁ (tm_var _) , Δ_{A} [ π₂ (tm_var _) ]tm ⟩ ]) (t₁ t₂ : tm Γ A) : t₁ ≡ t₂ ⊢ φ [ ⟨ tm_var _ , ⟨ t₁ , t₂ ⟩ ⟩ ]. Proof. pose (s := hyperdoctrine_eq_elim_help_con_sub Γ A). assert (⊤ ⊢ φ [s] [⟨ Δ_{ A } [ π₁ (tm_var _) ]tm , π₂ (tm_var _) ⟩]) as q. { unfold s, hyperdoctrine_eq_elim_help_con_sub. rewrite hyperdoctrine_comp_subst. rewrite hyperdoctrine_diag_subst. rewrite !hyperdoctrine_pair_subst. rewrite hyperdoctrine_pair_comp_pr2. rewrite !tm_subst_comp. rewrite !hyperdoctrine_pair_comp_pr1. rewrite hyperdoctrine_pair_comp_pr2. rewrite hyperdoctrine_diag_subst in p. pose (hyperdoctrine_proof_subst ⟨ π₂ (tm_var _) , π₁ (tm_var _) ⟩ p) as p'. rewrite truth_subst in p'. refine (hyperdoctrine_cut p' _). rewrite hyperdoctrine_comp_subst. rewrite !hyperdoctrine_pair_subst. rewrite hyperdoctrine_pair_comp_pr2. rewrite !hyperdoctrine_pair_comp_pr1. apply hyperdoctrine_hyp. } use (hyperdoctrine_cut (hyperdoctrine_eq_elim_help_con' (φ [ s ]) q t₁ t₂)). unfold s, hyperdoctrine_eq_elim_help_con_sub. rewrite hyperdoctrine_comp_subst. rewrite !hyperdoctrine_pair_subst. rewrite hyperdoctrine_pair_comp_pr2. rewrite !tm_subst_comp. rewrite !hyperdoctrine_pair_comp_pr1. rewrite hyperdoctrine_pair_comp_pr2. apply hyperdoctrine_hyp. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Projection. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseTerminal. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseInitial. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseProducts. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCoproducts. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCartesianClosed. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentProducts. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentSums. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Preservation.