- | elim (tdeq_inv_sort1 … H2) -H2 #x #d #Hs
- <(le_n_O_to_eq n) [| /2 width=3 by le_S_S_to_le/ ] -n #Hx #H destruct
- lapply (deg_next … Hs) #H
- lapply (deg_mono … H Hx) -H -Hx #Hd
- lapply (pred_inv_fix_sn … Hd) -Hd #H destruct
- /3 width=4 by refl, ex4_intro, or_intror/
+ | <(le_n_O_to_eq n) [| /2 width=3 by le_S_S_to_le/ ] -n
+ /3 width=3 by ex3_intro, or_intror/