elim (tdeq_inv_pair … H) -H #H destruct
| @or_intror @(ex2_intro … (ⓓ{p}ⓝW1.V1.U1)) [ /2 width=1 by cpm_beta/ ] #H
elim (tdeq_inv_pair … H) -H #H destruct
elim (tdeq_inv_pair … H) -H #H destruct
| @or_intror @(ex2_intro … (ⓓ{p}ⓝW1.V1.U1)) [ /2 width=1 by cpm_beta/ ] #H
elim (tdeq_inv_pair … H) -H #H destruct