Equality of maps and coherence theorem for biclosed categories

The problems in question are reduced here to ones for closed categories solved in [2,3]. First a natural deduction system is constructed and a term is assigned to any derivation. Equivalence relation ($\underset{BC}\equiv$) is defined for terms. Next a term is assigned to every canonical map and it is proved that two canonical maps are equal iff corresponding terms are equivalent. Finally, using the results from [2,3] we present decision algorithm for ($\underset{BC}\equiv$) and prove coherence theorem for canonical maps in ВС categories.