This also gets rid of [val_for_compare]-normalization; instead we introduce a
[LitErased] literal that is suited for use by erasure theorems.