{ intro hor
  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
⊢ B s ∧ Us = (S, s) ∨ ¬B s ∧ Us = (T, s) → (Stmt.ifThenElse B S T, s) ⇒ Us
no goals