apply RTC.head
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 (Stmt.skip; T, t) (Stmt.skip, u)
case seq.hbc.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)
⊢ (Stmt.skip; T, t) ⇒ ?seq.hbc.b

case seq.hbc.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.hbc.b (Stmt.skip, u)

case seq.hbc.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