apply RTC.trans
case seq
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ RTC SmallStep (S; T, s) (Stmt.skip, u)
case seq.hab
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ RTC SmallStep (S; T, s) ?seq.b

case seq.hbc
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ RTC SmallStep ?seq.b (Stmt.skip, u)

case seq.b
Ss : Stmt × State
t✝ : State
S T : Stmt
s t u : State
hS : (S, s) ⟹ t
hT : (T, t) ⟹ u
ihS : RTC SmallStep (S, s) (Stmt.skip, t)
ihT : RTC SmallStep (T, t) (Stmt.skip, u)
⊢ Stmt × State