[ * /3 width=2 by deg_SO_succ, ex_intro/
| /5 width=2 by deg_SO_zero, ex_intro/
]
| #s0 #d1 #d2 * [ #n1 ] #H1 * [1,3: #n2 ] #H2
[ < H2 in H1; -H2 #H
[ * /3 width=2 by deg_SO_succ, ex_intro/
| /5 width=2 by deg_SO_zero, ex_intro/
]
| #s0 #d1 #d2 * [ #n1 ] #H1 * [1,3: #n2 ] #H2
[ < H2 in H1; -H2 #H