proposition: Lemma composition_identity_right {Γ τ τ'} (f : Exp Γ (τ ⟶ τ')) : composition f (identity Γ τ) ≈ f.
proof: Proof. intro. now rewrite SemExp_composition. Qed.
imports: Category.Instance.Lambda.Ty Category.Instance.Lambda.Exp Category.Instance.Lambda.Ren Category.Instance.Lambda.Sem Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Structure.Terminal Category.Structure.Cartesian Category.Structure.Cartesian.Closed Category.Instance.Sets Category.Instance.Coq Equations(Equations)