:: deftheorem defines valH HENMODEL:def 6 :
for Al being QC-alphabet holds valH Al = id (bound_QC-variables Al);