proposition: Lemma composition_assoc_sym {Γ τ τ' τ'' τ'''} (f : Exp Γ (τ'' ⟶ τ''')) (g : Exp Γ (τ' ⟶ τ'')) (h : Exp Γ (τ ⟶ τ')) : composition (composition f g) h ≈ composition f (composition g h).
proof: Proof. intro. rewrite !SemExp_composition. now rewrite compose_assoc. 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)