Theorem: LoVe.SmallStep_skip (LoVe/Lectures/LoVe09_OperationalSemantics_Demo.lean)

State before:
S : Stmt
s t : State
⊢ ¬(Stmt.skip, s) ⇒ (S, t)
Tactic:
intro h
State after:
S : Stmt
s t : State
h : (Stmt.skip, s) ⇒ (S, t)
⊢ False

State before:
S : Stmt
s t : State
h : (Stmt.skip, s) ⇒ (S, t)
⊢ False
Tactic:
cases h
State after:
no goals