InsCode ((a,k1) := k2) = 7 by SCMPDS_2:19;
hence (a,k1) := k2 is shiftable by Def13; :: thesis: verum