Proposition tm_subst_comp {H : preorder_hyperdoctrine} {Γ₁ Γ₂ Γ₃ A : ty H} (s₁ : tm Γ₁ Γ₂) (s₂ : tm Γ₂ Γ₃) (t : tm Γ₃ A) : (t [ s₂ ]tm) [ s₁ ]tm = t [ s₂ [ s₁ ]tm ]tm. Proof. unfold tm_subst. apply assoc. 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.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Preservation.