cases h with
| inl h =>
  cases h with
  | intro hB hS =>
    apply BigStep.if_true <;>
      assumption
| inr h =>
  cases h with
  | intro hB hT =>
    apply BigStep.if_false <;>
      assumption
case mpr
B : State → Prop
S T : Stmt
s t : State
h : B s ∧ (S, s) ⟹ t ∨ ¬B s ∧ (T, s) ⟹ t
⊢ (Stmt.ifThenElse B S T, s) ⟹ t
no goals