- <(change_vec_same … tc src (niltape ?)) in Hd:(???(???(???%??)??));
- <(change_vec_same … tc dst (niltape ?)) in ⊢(???(???(???%??)??)→?);
- >Hdst_tc >Hsrc_tc >change_vec_change_vec >change_vec_change_vec
- >(change_vec_commute ?? tc ?? dst src) [|@(sym_not_eq … Hneq)]
+ <(change_vec_same … td src (niltape ?)) in Hd:(???(???(???%??)??));
+ <(change_vec_same … td dst (niltape ?)) in ⊢(???(???(???%??)??)→?);
+ >Hdst_tc >Hsrc_tc >(change_vec_change_vec ?) >change_vec_change_vec
+ >(change_vec_commute ?? td ?? dst src) [|@(sym_not_eq … Hneq)]