Proposition per_trans {X : ty H} {e : per X} {Γ : ty H} {Δ : form Γ} {s : tm Γ (X ×h X)} (t : tm Γ X) (p : Δ ⊢ e [ ⟨ π₁ s , t ⟩ ]) (q : Δ ⊢ e [ ⟨ t , π₂ s ⟩ ]) : Δ ⊢ e [ s ]. Proof. pose proof (pr22 e) as r₁. cbn in r₁. unfold per_trans_axiom in r₁. pose proof (hyperdoctrine_proof_subst (!! : tm Γ 𝟙) r₁) as r₂. clear r₁. rewrite truth_subst in r₂. rewrite !forall_subst in r₂. rewrite !impl_subst in r₂. rewrite !hyperdoctrine_comp_subst in r₂. rewrite !hyperdoctrine_pair_subst in r₂. rewrite !hyperdoctrine_pr2_subst in r₂. rewrite !hyperdoctrine_pr1_subst in r₂. rewrite !var_tm_subst in r₂. rewrite hyperdoctrine_pair_pr2 in r₂. rewrite !hyperdoctrine_pair_pr1 in r₂. rewrite !hyperdoctrine_pair_pr2 in r₂. pose proof (forall_elim r₂ (π₁ s)) as r₃. clear r₂. rewrite !forall_subst in r₃. rewrite !impl_subst in r₃. rewrite !hyperdoctrine_comp_subst in r₃. rewrite !hyperdoctrine_pair_subst in r₃. rewrite !hyperdoctrine_pr2_subst in r₃. rewrite !hyperdoctrine_pr1_subst in r₃. rewrite !var_tm_subst in r₃. rewrite !hyperdoctrine_pr1_subst in r₃. rewrite hyperdoctrine_pair_pr2 in r₃. rewrite !hyperdoctrine_pair_pr1 in r₃. rewrite !hyperdoctrine_pair_pr2 in r₃. rewrite !var_tm_subst in r₃. rewrite !hyperdoctrine_pair_pr1 in r₃. pose proof (forall_elim r₃ t) as r₄. clear r₃. rewrite !forall_subst in r₄. rewrite !impl_subst in r₄. rewrite !hyperdoctrine_comp_subst in r₄. rewrite !hyperdoctrine_pair_subst in r₄. rewrite !hyperdoctrine_pr2_subst in r₄. rewrite !hyperdoctrine_pr1_subst in r₄. rewrite !var_tm_subst in r₄. rewrite hyperdoctrine_pair_pr2 in r₄. rewrite !hyperdoctrine_pair_pr1 in r₄. rewrite !hyperdoctrine_pair_pr2 in r₄. rewrite !hyperdoctrine_pair_subst in r₄. rewrite !hyperdoctrine_pair_pr2 in r₄. rewrite !hyperdoctrine_pr1_subst in r₄. rewrite !tm_subst_comp in r₄. rewrite !hyperdoctrine_pr1_subst in r₄. rewrite !var_tm_subst in r₄. rewrite !hyperdoctrine_pair_pr1 in r₄. pose proof (forall_elim r₄ (π₂ s)) as r₅. clear r₄. rewrite !impl_subst in r₅. rewrite !hyperdoctrine_comp_subst in r₅. rewrite !hyperdoctrine_pair_subst in r₅. rewrite !hyperdoctrine_pr2_subst in r₅. rewrite !hyperdoctrine_pr1_subst in r₅. rewrite !var_tm_subst in r₅. rewrite hyperdoctrine_pair_pr2 in r₅. rewrite !tm_subst_comp in r₅. rewrite !hyperdoctrine_pr1_subst in r₅. rewrite !var_tm_subst in r₅. rewrite !hyperdoctrine_pair_pr1 in r₅. rewrite !tm_subst_var in r₅. pose proof (weaken_to_empty r₅ : Δ ⊢ _) as r₆. clear r₅. pose proof (impl_elim p r₆) as r₇. clear r₆. pose proof (impl_elim q r₇) as r₈. clear r₇. rewrite (hyperdoctrine_pair_eta s). exact r₈. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine.