cases hr with
| seq_step _ S _ _ s' hskip => cases hskip
| seq_skip                  => rfl
case seq_skip
Ss Ll : Stmt × State
T : Stmt
s : State
Rr : Stmt × State
hr : (Stmt.skip; T, s) ⇒ Rr
⊢ (T, s) = Rr
no goals