cases h with
| intro hB h =>
  cases h with
  | intro hS hwhile =>
    apply BigStep.while_true <;>
      assumption
case mpr.inl.intro
B : State → Prop
S : Stmt
s u t : State
h : B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u
⊢ (Stmt.whileDo B S, s) ⟹ u
no goals