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