-definition sd_SO: ∀h. nat → sd h ≝ λh,k. mk_sd h (deg_SO h k) ….
-[ #k0
- lapply (nexts_dec h k0 k) *
- [ * /3 width=2 by deg_SO_pos, ex_intro/ | /4 width=2 by deg_SO_zero, ex_intro/ ]
-| #K0 #d1 #d2 * [ #d01 ] #H1 * [1,3: #d02 ] #H2 //
+definition sd_SO: ∀h. nat → sd h ≝ λh,s. mk_sd h (deg_SO h s) ….
+[ #s0
+ lapply (nexts_dec h s0 s) *
+ [ * /3 width=2 by deg_SO_succ, ex_intro/ | /4 width=2 by deg_SO_zero, ex_intro/ ]
+| #K0 #d1 #d2 * [ #n1 ] #H1 * [1,3: #n2 ] #H2 //