cases hr with
| if_true  => rfl
| if_false => aesop
case if_true
Ss Ll : Stmt × State
B : State → Prop
S T : Stmt
s : State
hB : B s
Rr : Stmt × State
hr : (Stmt.ifThenElse B S T, s) ⇒ Rr
⊢ (S, s) = Rr
no goals