∃∃ri0,rs0,ti0,ts0. (ri0∨rs0) = ri & 0 = rs & (ti0∨ts0) = ti & 0 = ts &
〈ri0, rs0, ti0, ts0〉 = c.
#ri #rs #ti #ts * #ri0 #rs0 #ti0 #ts0 <shift_rew #H destruct
∃∃ri0,rs0,ti0,ts0. (ri0∨rs0) = ri & 0 = rs & (ti0∨ts0) = ti & 0 = ts &
〈ri0, rs0, ti0, ts0〉 = c.
#ri #rs #ti #ts * #ri0 #rs0 #ti0 #ts0 <shift_rew #H destruct