Proposition from_exp_comm_partial_setoid_weaken {Γ : ty H} (Δ χ : form Γ) (γ : tm Γ (prod_partial_setoid X Z ×h Y)) (Γ' := ((Γ ×h X ×h ℙ (X ×h Y)) ×h X) ×h Z) (x₁ := π₁ (π₂ (π₁ (π₁ (tm_var Γ'))))) (x₂ := π₂ (π₁ (tm_var Γ'))) (z := π₂ (tm_var Γ')) (δ := π₁ (π₁ (π₁ (tm_var Γ')))) (f := π₂ (π₂ (π₁ (π₁ (tm_var Γ'))))) (p : Δ [δ] ∧ exp_comm_partial_setoid_1 [⟨ γ [δ ]tm, ⟨ x₁ , f ⟩ ⟩] ∧ exp_comm_partial_setoid_3 [⟨ ⟨ γ [δ ]tm, ⟨ x₁ , f ⟩ ⟩, x₂ ⟩] ∧ exp_comm_partial_setoid_2 [⟨ ⟨ γ [δ ]tm, ⟨ x₁ , f ⟩ ⟩, z ⟩] ⊢ χ [δ]) : Δ ∧ exp_comm_partial_setoid [ γ ] ⊢ χ. Proof. unfold exp_comm_partial_setoid. rewrite !exists_subst. refine (exists_elim _ _). { use weaken_right. apply hyperdoctrine_hyp. } rewrite !conj_subst. use hyp_sym. use hyp_rtrans. use weaken_left. use hyp_sym. rewrite !exists_subst. refine (exists_elim _ _). { use weaken_right. use weaken_left. apply hyperdoctrine_hyp. } rewrite !conj_subst. refine (exists_elim _ _). { use weaken_left. do 2 use weaken_right. use weaken_left. rewrite exists_subst. apply hyperdoctrine_hyp. } rewrite !conj_subst. refine (hyperdoctrine_cut _ (hyperdoctrine_cut p _)). - repeat use conj_intro. + do 3 use weaken_left. simplify. apply hyperdoctrine_hyp. + do 2 use weaken_left. do 3 use weaken_right. simplify. unfold x₁, f. rewrite <- hyperdoctrine_pair_eta. apply hyperdoctrine_hyp. + use weaken_left. use weaken_right. unfold x₁, f. rewrite <- hyperdoctrine_pair_eta. simplify. apply hyperdoctrine_hyp. + use weaken_right. unfold x₁, f. rewrite <- hyperdoctrine_pair_eta. simplify. apply hyperdoctrine_hyp. - simplify. 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. Require Import UniMath.CategoryTheory.Hyperdoctrines.Tripos. Require Import UniMath.CategoryTheory.Hyperdoctrines.GenericPredicate. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERs. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERMorphisms. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERCategory. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERBinProducts. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.ExponentialPER. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.ExponentialEval. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.ExponentialLam.