apply Exists.intro S
case ifThenElse.inl
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
h : B s
⊢ ∃ T_1 t, (Stmt.ifThenElse B S T, s) ⇒ (T_1, t)
case ifThenElse.inl
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
h : B s
⊢ ∃ t, (Stmt.ifThenElse B S T, s) ⇒ (S, t)