cases hr with
| if_true  => aesop
| if_false => rfl
case if_false
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
⊢ (T, s) = Rr
no goals