cases hr with
| whileDo => rfl
case whileDo
Ss Ll : Stmt × State
B : State → Prop
S : Stmt
s : State
Rr : Stmt × State
hr : (Stmt.whileDo B S, s) ⇒ Rr
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) = Rr
no goals