(* Basic inversion properties ***********************************************)
lemma shift_inv_dx: ∀ri,rs,ti,ts,c. 〈ri, rs, ti, ts〉 = ↓c →
(* Basic inversion properties ***********************************************)
lemma shift_inv_dx: ∀ri,rs,ti,ts,c. 〈ri, rs, ti, ts〉 = ↓c →