[ /4 width=5 by snv_lref, drop_drop_lt/
| @snv_lref [4: // |1,2,3: skip ]
@snv_bind //
@(snv_appl … a … (⋆k) … (⋆k) (0+1))
[ @snv_lref [4: // |1,2,3: skip ] //
| @snv_lref [4: /2 width=1 by drop_drop_lt/ |1,2,3: skip ] @snv_bind //
[ /4 width=5 by snv_lref, drop_drop_lt/
| @snv_lref [4: // |1,2,3: skip ]
@snv_bind //
@(snv_appl … a … (⋆k) … (⋆k) (0+1))
[ @snv_lref [4: // |1,2,3: skip ] //
| @snv_lref [4: /2 width=1 by drop_drop_lt/ |1,2,3: skip ] @snv_bind //