- [ @deg_SO_zero #n >(sh_nexts_succ_next h n s0) #H
- lapply (sh_nexts_inj … Hha ???) -H #H destruct
- | #n @deg_SO_succ >sh_nexts_swap //
+ [ @deg_SO_zero #n >sh_nexts_succ_next #H
+ lapply (sh_nexts_inj … Hha … H) -H #H
+ elim (eq_inv_nsucc_zero … H)
+ | #n #_ /2 width=1 by deg_SO_succ/