[ #J #H destruct
| #J #W #U #IHW #_ #H destruct
-H >e0 in e1; normalize (**) (* destruct: one quality is not simplified, the destucted equality is not erased *)
[ #J #H destruct
| #J #W #U #IHW #_ #H destruct
-H >e0 in e1; normalize (**) (* destruct: one quality is not simplified, the destucted equality is not erased *)