{ intro h
  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
⊢ (Stmt.ifThenElse B S T, s) ⟹ t → B s ∧ (S, s) ⟹ t ∨ ¬B s ∧ (T, s) ⟹ t

case mpr
B : State → Prop
S T : Stmt
s t : State
⊢ B s ∧ (S, s) ⟹ t ∨ ¬B s ∧ (T, s) ⟹ t → (Stmt.ifThenElse B S T, s) ⟹ t
case mpr
B : State → Prop
S T : Stmt
s t : State
⊢ B s ∧ (S, s) ⟹ t ∨ ¬B s ∧ (T, s) ⟹ t → (Stmt.ifThenElse B S T, s) ⟹ t