cases Classical.em (B s) with
| inl h =>
  apply Exists.intro S
  apply Exists.intro s
  apply SmallStep.if_true
  assumption
| inr h =>
  apply Exists.intro T
  apply Exists.intro s
  apply SmallStep.if_false
  assumption
case ifThenElse
s : State
B : State → Prop
S T : Stmt
ihS : (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = Stmt.skip
ihT : (¬∃ T_1 t, (T, s) ⇒ (T_1, t)) ↔ T = Stmt.skip
⊢ ∃ T_1 t, (Stmt.ifThenElse B S T, s) ⇒ (T_1, t)
no goals