:: deftheorem defines HCar HENMODEL:def 4 :
for Al being QC-alphabet holds HCar Al = bound_QC-variables Al;