cases h with
| inl hex =>
  cases hex with
  | intro t h =>
    cases h with
    | intro hB h =>
      cases h with
      | intro hS hwhile =>
        apply BigStep.while_true <;>
          assumption
| inr h =>
  cases h with
  | intro hB hus =>
    rw [hus]
    apply BigStep.while_false
    assumption
case mpr
B : State → Prop
S : Stmt
s u : State
h : (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u) ∨ ¬B s ∧ u = s
⊢ (Stmt.whileDo B S, s) ⟹ u
no goals