rw [BigStep_while_Iff]
B : State → Prop
S : Stmt
s u : State
hcond : B s
⊢ (Stmt.whileDo B S, s) ⟹ u ↔ ∃ t, (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u
B : State → Prop
S : Stmt
s u : State
hcond : B s
⊢ (∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u) ∨ ¬B s ∧ u = s ↔ ∃ t, (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u