cases h with
| if_true _ _ _ _ _ hB hS =>
  apply Or.intro_left
  aesop
| if_false _ _ _ _ _ hB hT =>
  apply Or.intro_right
  aesop
case mp
B : State → Prop
S T : Stmt
s t : State
h : (Stmt.ifThenElse B S T, s) ⟹ t
⊢ B s ∧ (S, s) ⟹ t ∨ ¬B s ∧ (T, s) ⟹ t
no goals