assumption
case seq.inr.intro.intro.hS
s : State
S T : Stmt
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
h : ¬S = Stmt.skip
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
⊢ (S, s) ⇒ (S', s')
no goals