{ intro h
  cases h with
  | if_true _ _ _ _ hB  => aesop
  | if_false _ _ _ _ hB => aesop }
case mp
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
⊢ (Stmt.ifThenElse B S T, s) ⇒ Us → B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s)

case mpr
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
⊢ B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s) → (Stmt.ifThenElse B S T, s) ⇒ Us
case mpr
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
⊢ B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s) → (Stmt.ifThenElse B S T, s) ⇒ Us