proposition: Theorem Ctxt_comp_assoc {Γ τ τ' τ'' τ'''} {C : Ctxt Γ τ' τ} {C' : Ctxt Γ τ'' τ'} {C'' : Ctxt Γ τ''' τ''} : Ctxt_comp C (Ctxt_comp C' C'') = Ctxt_comp (Ctxt_comp C C') C''.
proof: Proof. induction C; simpl; auto; now f_equal. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Ltac Category.Instance.Lambda.Ty Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Sub Equations(Equations)