lapply (tog_total ??? e);
lapply (tog_total ??? Hletin);
lapply (ltplus ????? Hletin2 Hletin1);
apply (exc_rewl ??? (0+0)); [apply eq_sym; apply zero_neutral]
lapply (tog_total ??? e);
lapply (tog_total ??? Hletin);
lapply (ltplus ????? Hletin2 Hletin1);
apply (exc_rewl ??? (0+0)); [apply eq_sym; apply zero_neutral]