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