apply RTC.lift (fun Ss ↦ (Prod.fst Ss; T, Prod.snd Ss)) _ h
S T : Stmt
s u : State
h : RTC SmallStep (S, s) (Stmt.skip, u)
⊢ RTC SmallStep (S; T, s) (Stmt.skip; T, u)
S T : Stmt
s u : State
h : RTC SmallStep (S, s) (Stmt.skip, u)
⊢ ∀ (a b : Stmt × State), a ⇒ b → (fun Ss => (Ss.fst; T, Ss.snd)) a ⇒ (fun Ss => (Ss.fst; T, Ss.snd)) b