By default, no confluence checking, even if CSI^HO is installed

dk_binary_nat because it is hard to prove confluent and dk_binary_nat is
not checked for confluence.

Comment hard to check rules and fix a confluence bug in dk_machine_int.

Move rules on cc.eT to better locations so that cc.dk only talk about
dependent product and arrow.

yet work)

between .dk and .dko file names

terms in cc.uT

-> Expr