fact: Definition composition {Γ τ τ' τ''} (f : Exp Γ (τ' ⟶ τ'')) (g : Exp Γ (τ ⟶ τ')) : Exp Γ (τ ⟶ τ'') := LAM (APP (wk f) (APP (wk g) (VAR ZV))).
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)