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