Proposition per_sym {X : ty H} {e : per X} {Γ : ty H} {Δ : form Γ} {s : tm Γ (X ×h X)} (p : Δ ⊢ e [ ⟨ π₂ s , π₁ s ⟩ ]) : Δ ⊢ e [ s ]. Proof. pose proof (pr12 e) as q. unfold per_symm_axiom in q. pose proof (hyperdoctrine_proof_subst (!! : tm Γ 𝟙) q) as q'. clear q. rewrite truth_subst in q'. rewrite !forall_subst in q'. rewrite impl_subst in q'. rewrite !hyperdoctrine_comp_subst in q'. rewrite !hyperdoctrine_pair_subst in q'. pose proof (forall_elim q' (π₂ s)) as r. clear q'. 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_subst in r. rewrite !hyperdoctrine_pr2_subst in r. rewrite !hyperdoctrine_pr1_subst 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. rewrite !hyperdoctrine_pair_pr2 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 !var_tm_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'. rewrite tm_subst_var in r'. rewrite hyperdoctrine_pair_pr2 in r'. pose proof (weaken_to_empty r' : Δ ⊢ _) as r''. clear r'. pose proof (impl_elim p 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.