cases hor with
| inl hand =>
  cases hand with
  | intro hB hUs =>
    rw [hUs]
    apply SmallStep.if_true
    assumption
| inr hand =>
  cases hand with
  | intro hB hUs =>
    rw [hUs]
    apply SmallStep.if_false
    assumption
case mpr
B : State → Prop
S T : Stmt
s : State
Us : Stmt × State
hor : B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s)
⊢ (Stmt.ifThenElse B S T, s) ⇒ Us
no goals