fact: Definition app_as_csb_fun: (CSetoid_bin_fun free_csetoid_as_csetoid free_csetoid_as_csetoid free_csetoid_as_csetoid):= (Build_CSetoid_bin_fun free_csetoid_as_csetoid free_csetoid_as_csetoid free_csetoid_as_csetoid appA app_strext).
imports: CoRN.algebra.CSetoids