∀src,dst,sig,n,is_sep,v,t.src ≠ dst → src < S n → dst < S n →
∀s.current ? t = Some ? s → is_sep s = false →
step sig n (copy_step src dst sig n is_sep)
∀src,dst,sig,n,is_sep,v,t.src ≠ dst → src < S n → dst < S n →
∀s.current ? t = Some ? s → is_sep s = false →
step sig n (copy_step src dst sig n is_sep)